log_phi_gt_0481
plain-language theorem explainer
Lemma establishes the inequality 0.481 < log φ where φ is the golden ratio constant. Interval specialists refining bounds on the inverse fine-structure constant cite this result when deriving tighter lower estimates for gap terms. The short tactic proof rewrites via the log-exp equivalence then chains a Taylor upper bound on exp(0.481) with the decimal lower bound φ > 1.61803395 using transitivity.
Claim. $0.481 < log φ$ where $φ$ is the golden ratio constant satisfying $φ = (1 + √5)/2$.
background
The module supplies rigorous interval bounds on the inverse fine-structure constant α^{-1} derived from the Recognition Science symbolic framework. The golden ratio φ enters as the self-similar fixed point (T6) in the forcing chain, with numerical value near 1.6180339887. Upstream results include the decimal lower bound φ > 1.61803395 from W8Bounds.phi_gt_161803395 together with the Taylor-derived comparison exp(0.481) < 1.6177... from exp_0481_lt.
proof idea
Rewrite the goal using the equivalence log x > y ↔ x > exp(y) for x > 0. Obtain the lower bound φ > 1.61803395 from W8Bounds.phi_gt_161803395 via linarith. Conclude by applying lt_trans to exp_0481_lt and the phi lower bound.
why it matters
This bound feeds directly into f_gap_gt_strong to sharpen the lower estimate on the gap term used in alpha interval calculations. It supports numerical verification of the α^{-1} band inside (137.030, 137.039) and links the phi-ladder numerics to the eight-tick octave structure. The claim is fully proved with no remaining scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.