phi76_lt
plain-language theorem explainer
The lemma establishes that the golden ratio to the 76th power is strictly less than 7646046000000000 in the reals. Researchers checking lepton mass predictions against PDG data in the Recognition Science mass ladder would cite this bound for the tau rung verification. The proof is a one-line wrapper that rewrites the RS constant phi via its equality to goldenRatio and invokes the precomputed numerical bound.
Claim. Let $phi$ denote the golden ratio. Then $phi^{76} < 7646046000000000$.
background
In the Masses.Verification module, lepton masses follow the integer-rung formula m(Lepton, r) = phi^(57+r) / (2^22 * 10^6) in MeV, with experimental values treated as imported constants rather than derived. The RS constant phi is identified with the golden ratio by the lemma phi_eq_goldenRatio, which unfolds the definition and applies ring simplification. Upstream results include the structure Constants from CPM.LawOfExistence and the numerical theorem phi_pow76_lt in Numerics.Interval.PhiBounds, which factors the power as phi^70 * phi^6 and chains prior bounds on those exponents.
proof idea
The term-mode proof applies rw [phi_eq_goldenRatio] to replace Constants.phi with goldenRatio, then uses exact to discharge the goal with the theorem phi_pow76_lt from the numerics module. That theorem itself proceeds by ring_nf factoring, application of phi_pow70_lt and phi_pow6_lt, and positivity to confirm the product inequality.
why it matters
This lemma feeds directly into tau_mass_bounds, which establishes the interval (1821, 1823) for the predicted tau mass in MeV and thereby closes the numerical check for the tau rung in the lepton sector. It supports the overall mass-ladder verification against PDG 2024 data, consistent with the phi-ladder construction and the self-similar fixed point from the forcing chain. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.