phi59_lt
plain-language theorem explainer
The lemma asserts that the Recognition Science constant phi raised to the 59th power is strictly less than 2139810000000. Lepton mass verification routines cite this bound to confirm that the predicted electron mass lies inside the PDG experimental interval. The proof is a one-line wrapper that rewrites phi to the golden ratio and invokes a pre-established numerical inequality.
Claim. Let $phi$ be the golden ratio. Then $phi^{59} < 2139810000000$.
background
The Verification module compares Recognition Science mass predictions to PDG 2024 experimental values for leptons. The integer-rung formula is m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6) MeV, with B_pow = -22 and r0 = 62. This supplies a numerical upper bound on phi^59 that supports checking the electron mass interval (r = 2 yields exponent 59). Upstream phi_eq_goldenRatio lemmas from Astrophysics.ObservabilityLimits, ElectroweakMasses, and the local module each equate Constants.phi to goldenRatio or Real.goldenRatio. The key dependency is phi_pow59_lt from Numerics.Interval.PhiBounds, which proves the same inequality for goldenRatio via decomposition into phi_pow51_lt and phi_pow8_lt.
proof idea
The proof is a one-line wrapper. The rw [phi_eq_goldenRatio] tactic substitutes Constants.phi with goldenRatio. The exact tactic then discharges the goal by applying the theorem phi_pow59_lt from Numerics.Interval.PhiBounds.
why it matters
This lemma is invoked by electron_mass_bounds to establish the interval (0.5098, 0.5102) for the electron mass prediction. It closes a numerical verification step in the lepton sector, consistent with the phi-ladder mass formula and the self-similar fixed point phi from the forcing chain (T6). The module remains quarantined from the certified surface because experimental values are imported constants rather than derived from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.