ideal_hcp_ratio_value
plain-language theorem explainer
The theorem establishes that the ideal HCP c/a ratio, defined as the square root of 8/3, lies strictly between 1.63 and 1.64. Crystallographers and materials modelers would cite it when benchmarking observed HCP lattices against the geometric ideal from close packing. The proof unfolds the definition, reduces both sides of the target inequality to squared comparisons via norm_num, and applies the monotonicity of the positive square root to finish.
Claim. The ideal HCP c/a ratio satisfies $1.63 < √(8/3) < 1.64$.
background
In the Crystal Structure Stability module, BCC, FCC, and HCP lattices arise from RS coordination rules. BCC uses 8-tick coordination while FCC and HCP achieve close packing with coordination 12 and packing fraction π/(3√2) ≈ 0.74. The ideal HCP c/a ratio is introduced as √(8/3) to quantify the geometric height-to-base ratio that equalizes nearest-neighbor distances in the hexagonal cell. The module states that this ratio is approximately 1.633 and lies near φ, with deviations signaling anisotropic bonding.
proof idea
The tactic proof first applies simp to replace idealHCPRatio by Real.sqrt (8/3). It then constructs two auxiliary facts by norm_num: (1.63)^2 < 8/3 and 8/3 < (1.64)^2. The left half of the goal is discharged by rewriting with Real.lt_sqrt (after a positivity check), while the right half uses Real.sqrt_lt' (again after positivity) to reduce to the second squared inequality.
why it matters
The result supplies the concrete numerical bound required by the module's φ-stability prediction for HCP lattices. It anchors the claim that the ideal ratio ≈ 1.633 is close to φ, thereby linking the eight-tick octave and close-packing geometry to observable crystal metrics. No downstream theorems depend on it yet, but it closes the numerical verification step inside the CM-001 predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.