bcc_packing_lt_fcc
The result establishes that the approximate packing efficiency assigned to BCC lattices is strictly smaller than the value assigned to FCC lattices. Materials physicists comparing metallic crystal stability under Recognition Science principles would cite this ordering when discussing cohesive energy differences. The proof is a one-line wrapper that unfolds the packingEfficiencyApprox definition and evaluates the resulting numerical comparison.
claimLet $0.68$ be the approximate packing efficiency of body-centered cubic structures and $0.74$ the approximate packing efficiency of face-centered cubic structures. Then $0.68 < 0.74$.
background
The module Crystal Structure Stability (CM-001) derives BCC, FCC, and HCP lattices from Recognition Science mechanisms. BCC coordination equals 8 and reflects the eight-tick ledger period, while FCC and HCP achieve close packing with coordination 12. Packing efficiency is defined to relate directly to cohesive energy, with the ordering FCC ≈ HCP > BCC. The upstream definition packingEfficiencyApprox supplies the concrete values: BCC maps to 0.68 and both FCC and HCP map to 0.74.
proof idea
The proof is a one-line wrapper that applies simp only on packingEfficiencyApprox to substitute the case distinction, then norm_num to compare the resulting constants 0.68 and 0.74.
why it matters in Recognition Science
The theorem supplies the concrete numerical step that realizes the module prediction FCC = HCP ≈ 0.74 > BCC ≈ 0.68. It therefore supports the energy-ordering claim that close-packed structures are favored over eight-tick BCC structures. The result sits inside the T7 eight-tick octave and the coordination distinction between 8 and 12, but carries no downstream uses in the current graph.
scope and limits
- Does not derive the numerical packing values from the Recognition functional equation or J-cost.
- Does not address temperature dependence or phase transitions in real metals.
- Does not compare the assigned values against measured packing fractions of specific materials.
- Does not extend the comparison to other lattices such as simple cubic.
formal statement (Lean)
73theorem bcc_packing_lt_fcc : packingEfficiencyApprox .BCC < packingEfficiencyApprox .FCC := by
proof body
Term-mode proof.
74 simp only [packingEfficiencyApprox]
75 norm_num
76
77/-- FCC and HCP have same packing. -/