log_phi_gt_048
plain-language theorem explainer
The theorem establishes that the natural logarithm of the golden ratio exceeds 0.48. Numerics researchers in Recognition Science cite this when tightening interval bounds on logarithmic expressions involving phi for applications like critical temperature estimates. The proof rewrites the claim using the equivalence log(phi) > 0.48 iff phi > exp(0.48), then bounds the exponential via a 10-term Taylor series plus remainder and compares against a rational lower bound for phi.
Claim. $0.48 < log φ$ where $φ = (1 + √5)/2$ is the golden ratio.
background
This module develops rigorous interval arithmetic for the natural logarithm using Taylor expansions and error bounds from Mathlib. For log(φ) with φ the golden ratio, the approach exploits monotonicity of log and bounds the equivalent exponential inequality. Upstream results include the definition of exp_taylor_10_at_048 as the partial sum 1 + x + ... + x^9/9! at x=0.48 and the corresponding error term exp_error_10_at_048 = x^10 * 11 / (10! * 10), together with the lemma exp_048_lt_phi establishing the strict inequality of the Taylor sum plus error against 1.61803395.
proof idea
The proof applies the equivalence Real.lt_log_iff_exp_lt to reduce to showing exp(0.48) < phi. It invokes Real.exp_bound' with n=10 to obtain the Taylor sum plus remainder bound, equates the sum and error to the precomputed constants exp_taylor_10_at_048 and exp_error_10_at_048 via norm_num, then chains the inequality through exp_048_lt_phi to reach 1.61803395 and finally applies phi_gt_161803395.
why it matters
This bound supplies the lower estimate log(φ) > 0.48 that feeds into downstream results such as the BCS ratio approximation in SuperconductingTc, the gap function lower bound f_gap_gt, and the stiffness bounds gcic_stiffness_bounds in the GCIC Thermodynamics paper. It closes a numerical step in the phi-ladder construction of Recognition Science, where phi appears as the self-similar fixed point (T6) and supports the eight-tick octave structure. The result touches the open question of how tightly the alpha inverse band (137.03, 137.039) can be pinned using these logarithmic intervals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.