log_phi_gt_048
plain-language theorem explainer
The lemma establishes that log(φ) > 0.48 where φ denotes the golden ratio. Interval numerics and thermodynamic calculations in the Recognition framework cite this bound to anchor gap functions and stiffness estimates. The proof rewrites the claim via exponential monotonicity and chains a Taylor upper bound on exp(0.48) with the lower bound φ > 1.61803395 using transitivity.
Claim. $0.48 < log φ$ where $φ = (1 + √5)/2$ is the golden ratio constant.
background
The AlphaBounds module develops rigorous interval bounds on α⁻¹ using the Recognition Science constants. This lemma supplies a concrete lower bound on log(φ) that enters downstream gap and critical temperature estimates. Upstream results include exp_048_lt, which asserts exp(0.48) < 1.6161... via a 10-term Taylor series, and phi_gt_161803395, which asserts 1.61803395 < φ. The transitivity result lt_trans chains these inequalities.
proof idea
The proof rewrites the target via Real.lt_log_iff_exp_lt to obtain the equivalent exp(0.48) < φ. It extracts a lower bound on φ from W8Bounds.phi_gt_161803395 by linarith. The final step applies lt_trans to combine this lower bound with the Taylor-derived exp_048_lt.
why it matters
This bound feeds the BCS ratio approximation in Chemistry.SuperconductingTc and the stiffness bounds in Papers.GCIC.Thermodynamics. It anchors the self-similar fixed point φ from the forcing chain and supports interval arithmetic for α⁻¹. The result closes a concrete numerical step in the phi-ladder numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.