idealHCPRatio
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not derive the ratio from Recognition Science axioms or the forcing chain.
- Does not model temperature, pressure, or bonding anisotropy in real crystals.
- Does not compute packing fractions or coordination numbers.
- Does not address stacking faults or polytypism in HCP structures.
Lean usage
theorem hcp_ratio_near_phi : |idealHCPRatio - phi| < 0.03 := by simp only [idealHCPRatio]formal statement (Lean)
83def idealHCPRatio : ℝ := Real.sqrt (8/3)
proof body
Definition body.
84
85/-- The ideal HCP c/a ratio is approximately 1.633. -/