phi76_gt
plain-language theorem explainer
The lemma establishes the numerical bound 7638724000000000 < phi^76 in the reals, with phi the golden ratio. Researchers verifying Recognition Science lepton mass predictions against PDG data cite this result when checking the tau interval. The proof is a one-line wrapper that rewrites Constants.phi via the golden-ratio identification and invokes the corresponding theorem from the PhiBounds numerics module.
Claim. $7638724000000000 < phi^{76}$, where $phi$ denotes the golden ratio.
background
The Masses.Verification module compares RS lepton mass predictions to PDG 2024 values while treating experimental numbers as imported constants. The local formula is m(Lepton, r) = phi^{57+r} / (2^{22} * 10^6) in MeV for B_pow = -22 and r0 = 62. Constants.phi is identified with the golden ratio by the sibling lemma phi_eq_goldenRatio, which unfolds the definition and applies ring. The upstream theorem phi_pow76_gt from Numerics.Interval.PhiBounds supplies the core inequality directly for goldenRatio^76.
proof idea
This is a one-line wrapper proof. It applies the rewrite phi_eq_goldenRatio to replace Constants.phi by goldenRatio, then uses exact to discharge the goal with the theorem phi_pow76_gt.
why it matters
The bound is required by the downstream theorem tau_mass_bounds, which confirms the predicted tau mass lies in (1821, 1823) MeV. It supplies a concrete numerical step in the lepton-sector verification of the phi-ladder mass formula and connects to the self-similar fixed point phi (T6) in the forcing chain. No open scaffolding questions are closed by this lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.