log_phi_bounds
plain-language theorem explainer
The lemma establishes tight numerical bounds 0.481211 < log φ < 0.481213 on the natural logarithm of the golden ratio, conditional on two auxiliary hypotheses that bound log at the nearby constants 1.618033 and 1.618034. Physicists verifying lepton mass ladders or gap residues in the Recognition framework cite it to anchor floating-point precision in phi-powered formulas. The proof extracts the hypothesis bounds via simpa, invokes log monotonicity on the interval supplied by phi_bounds, and chains the resulting inequalities with lt_trans.
Claim. Assuming the lower numerical hypothesis $0.481211 < log(1.618033)$ and the upper numerical hypothesis $log(1.618034) < 0.481213$, it holds that $0.481211 < log φ < 0.481213$.
background
The module RSBridge.GapProperties supplies Lean-checked analytic properties of the structural residue gap(Z) := log(1 + Z/φ) / log φ, the zero-parameter Recognition-side function f^{Rec} used in mass formulas. Upstream phi_bounds (from Astrophysics.MassToLight and ElectronMass.Necessity) supplies the tight interval 1.618033 < φ < 1.618034 that makes the logarithm strictly increasing on the relevant domain. A sibling log_phi_bounds in ElectronMass.Necessity gives a slightly narrower target interval; the present lemma factors the numerical work into reusable hypotheses so that gap computations remain fully verified.
proof idea
The tactic proof first obtains phi_bounds, then uses simpa to unpack the two supplied hypotheses into explicit inequalities on log(1.618033) and log(1.618034). It applies Real.log_lt_log (with positivity from phi_bounds) to obtain log(1.618033) < log φ and log φ < log(1.618034), and finally chains each side with lt_trans to reach the target numerical bounds.
why it matters
The result is invoked by gap_1332_bounds in ElectronMass.Necessity and by the suite of phi_pow_neg theorems (phi_pow_neg375_upper_proved, phi_pow_neg3760_upper_v2, phi_pow_neg3762_lower_v2, phi_pow_neg377_lower_proved, etc.) in LeptonGenerations.Necessity. These downstream statements close numerical verification steps in the phi-ladder mass formula yardstick · φ^(rung − 8 + gap(Z)). It thereby supports the T6 self-similar fixed-point property of φ and the numerical consistency checks inside the alpha band (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.