idealHCPRatio
plain-language theorem explainer
The declaration defines the ideal c/a ratio for HCP crystal structures as the square root of eight thirds. Materials scientists and Recognition Science researchers comparing lattice geometry to phi would cite this constant when quantifying stability in close-packed phases. It enters as a direct definition of the standard crystallographic expression with no additional lemmas required.
Claim. The ideal $c/a$ ratio for hexagonal close-packed crystal structures is given by $√(8/3)$.
background
The Crystal Structure Stability module derives BCC, FCC, and HCP lattices from RS principles. Eight-tick coordination fixes BCC at coordination number 8, while close-packing yields coordination 12 for both FCC and HCP with maximum packing efficiency π/(3√2) ≈ 0.74. The φ-Stability section states that the ideal HCP c/a ratio is √(8/3) ≈ 1.633 ≈ φ, with deviations signaling anisotropic bonding. Energy ordering places FCC ≈ HCP above BCC in cohesive strength.
proof idea
This is a direct definition that sets the constant to Real.sqrt (8/3). No lemmas or tactics are invoked; the value is introduced by the expression itself.
why it matters
The definition supplies the exact operand for the parent theorem hcp_ratio_near_phi, which bounds |idealHCPRatio - phi| < 0.03, and for ideal_hcp_ratio_value, which places the ratio between 1.63 and 1.64. It realizes the φ-Stability prediction listed in the module's CM-001 framework and connects HCP geometry to the eight-tick octave and the phi fixed point from the forcing chain. It leaves open the quantitative match between this ideal and observed c/a ratios in real materials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.