phi70_lt
plain-language theorem explainer
The lemma asserts that the golden ratio to the 70th power is strictly less than 426011000000000. Researchers verifying lepton mass predictions in the Recognition Science framework cite this bound when checking the muon interval. The proof is a one-line wrapper that rewrites the RS phi constant to the standard golden ratio and applies a pre-established numerical inequality.
Claim. Let $phi$ denote the golden ratio. Then $phi^{70} < 426011000000000$.
background
The module compares RS lepton mass predictions to PDG 2024 data. The formula for the lepton sector with B_pow = -22 and r0 = 62 is m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6) in MeV. The constant phi appears in the Constants structure and is identified with the golden ratio by upstream lemmas such as 'Constants.phi equals Mathlib's goldenRatio (same definition)'.
proof idea
The proof is a one-line wrapper. It rewrites Constants.phi via the phi_eq_goldenRatio lemma to obtain goldenRatio, then applies the exact theorem phi_pow70_lt from Numerics.Interval.PhiBounds.
why it matters
This bound is invoked inside the muon_mass_bounds theorem to confirm the predicted muon mass lies in (101.49, 101.57). It supplies a numerical anchor for the phi-ladder mass formula in the lepton sector and closes a verification step that relies on the T6 phi fixed point. The result supports the overall comparison of RS predictions against experimental data without deriving the masses themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.