hcp_ratio_near_phi
plain-language theorem explainer
Materials scientists modeling HCP crystal stability under Recognition Science cite the bound showing the ideal c/a ratio lies within 0.03 of the golden ratio. The ideal ratio equals the square root of eight thirds while phi satisfies the supplied interval bounds 1.61 less than phi less than 1.62. The tactic proof first rewrites the definition, establishes the square root exceeds phi via an auxiliary comparison to 1.63, then applies the upper bound 1.64 together with linarith to close the difference estimate.
Claim. $|r - phi| < 0.03$ where $r = sqrt(8/3)$ is the ideal c/a ratio for hexagonal close-packed structures and $phi$ is the golden ratio.
background
The Crystal Structure Stability module derives BCC, FCC, and HCP lattices from RS principles. Close-packing yields coordination 12 and maximum packing fraction pi over 3 sqrt(2) approximately 0.74, while the phi-Stability paragraph states that the ideal c/a ratio for HCP satisfies sqrt(8/3) approximately 1.633 approximately phi. Upstream, idealHCPRatio is defined exactly as Real.sqrt (8/3) and the tighter bounds phi greater than 1.61 and phi less than 1.62 are established by direct comparison of sqrt(5) to 2.22 and 2.24 respectively.
proof idea
The tactic proof begins by simp only on idealHCPRatio to expose sqrt(8/3). It invokes phi_lt_onePointSixTwo to obtain phi less than 1.62, proves 1.63 less than sqrt(8/3) by Real.lt_sqrt and norm_num, deduces sqrt(8/3) greater than phi by linarith, rewrites the absolute value using abs_of_pos, then establishes sqrt(8/3) less than 1.64 by Real.sqrt_lt and norm_num together with phi greater than 1.61 from phi_gt_onePointSixOne, and finishes with linarith.
why it matters
The declaration fills the phi-Stability prediction inside the Crystal Structure Stability section (CM-001) of the module, where deviation from the ideal ratio signals anisotropic bonding. It links the HCP c/a value to the self-similar fixed point phi forced at T6 of the UnifiedForcingChain after J-uniqueness at T5. No downstream theorems are recorded, leaving open whether the numerical proximity will be used to bound energyScale or to compare FCC versus HCP cohesion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.