phi70_gt
plain-language theorem explainer
The lemma establishes a strict numerical lower bound on the golden ratio to the power 70, namely that 425698000000000 is less than phi^70. Mass verification routines in the Recognition Science lepton predictions cite this result to close interval bounds on predicted masses. The proof is a one-line wrapper applying a rewrite to the golden ratio definition and invoking a pre-established numerical theorem.
Claim. $425698000000000 < phi^{70}$, where $phi$ denotes the golden ratio.
background
The module verifies mass predictions against PDG 2024 data for the lepton sector using the formula $m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6)$ in MeV, with experimental values treated as imported constants. Constants.phi is identified with the golden ratio via the lemma phi_eq_goldenRatio, which unfolds the definition and applies ring simplification. Upstream numerical bounds from PhiBounds supply concrete inequalities for high powers of the golden ratio, enabling machine-checked comparisons.
proof idea
This is a one-line wrapper proof. It rewrites Constants.phi using phi_eq_goldenRatio to obtain the golden ratio, then applies the exact theorem phi_pow70_gt from the Numerics.Interval.PhiBounds module.
why it matters
The result is invoked by the muon_mass_bounds theorem to establish tight bounds on the predicted muon mass. It supports the phi-ladder construction in the mass formula with rung adjustments for the lepton sector. In the broader framework it anchors the numerical verification step following the self-similar fixed point for phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.