theorem proved term proof

`fcc_hcp_same_packing`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  78theorem fcc_hcp_same_packing : packingEfficiencyApprox .FCC = packingEfficiencyApprox .HCP := rfl

Term-mode proof.

  79
  80/-! ## HCP c/a Ratio and φ Connection -/
  81
  82/-- Ideal c/a ratio for HCP: √(8/3) ≈ 1.633. -/

Lean names referenced from this declaration's body.

packingEfficiencyApprox in IndisputableMonolith.Chemistry.CrystalStructure decl_use
for in IndisputableMonolith.Foundation.UniversalForcingSelfReference decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use