log_phi_bounds
plain-language theorem explainer
Bounds on the natural logarithm of the golden ratio are fixed as 0.481211 < log φ < 0.481212. Researchers deriving lepton mass spectra or electron gap values on the phi-ladder cite this to control exponential error terms. The tactic proof applies monotonicity of the logarithm to the interval 1 < φ < 2 and chains the resulting inequalities to precomputed numerical bounds via transitivity.
Claim. The natural logarithm of the golden ratio satisfies $0.481211 < log φ < 0.481212$, where $φ = (1 + √5)/2$.
background
The golden ratio φ satisfies 1 < φ < 2 by the upstream theorem stating φ is strictly between 1 and 2. This interval is obtained from the quadratic definition and used here to bound the logarithm. In the Recognition Science setting the module proves T9 necessity: the electron mass formula is forced from T8 ledger quantization together with geometric constants from the forcing chain.
proof idea
The proof invokes the interval 1 < φ < 2 and positivity of φ. It applies the strict increase of the logarithm to sandwich log φ between log(1.618033) and log(1.618034). Transitivity then combines these comparisons with the numerical lower and upper bounds to close the target interval.
why it matters
The bound feeds gap_1332_bounds for the electron mass gap and multiple phi_pow_neg theorems that establish lepton generation necessities. It supplies the precision step required by the T9 module, connecting to the phi fixed point in the forcing chain and the mass formula on the phi-ladder. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.