phi70_lt
The lemma bounds the golden ratio to the 70th power strictly below 426011000000000. It is cited inside the muon mass verification to confirm the RS lepton prediction sits inside the experimental window (101.49, 101.57). The proof is a one-line wrapper that rewrites the RS constant phi to the golden ratio and hands the inequality to a pre-established numeric theorem.
claimLet $phi$ denote the golden ratio. Then $phi^{70} < 426011000000000$.
background
The Masses.Verification module compares RS lepton mass predictions against PDG 2024 values. The formula used is m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6) in MeV, with experimental masses imported as constants rather than derived. The constant phi is shown equal to the golden ratio by the lemma that equates Constants.phi to Real.goldenRatio, appearing in this module, ElectroweakMasses, and ObservabilityLimits. The upstream numeric result phi_pow70_lt supplies the identical strict inequality for the golden ratio itself.
proof idea
One-line wrapper that rewrites Constants.phi to goldenRatio via the phi-equals-golden-ratio lemma, then applies the exact numeric bound phi_pow70_lt from Numerics.Interval.PhiBounds.
why it matters in Recognition Science
The bound supplies the ceiling required by the muon_mass_bounds theorem, which verifies that the predicted muon mass lies between 101.49 and 101.57. This closes a numeric step in the phi-ladder mass formula for the lepton sector (B_pow = -22, r0 = 62) and supports the Recognition Science comparison of integer-rung predictions against PDG data.
scope and limits
- Does not derive the inequality from the Recognition functional equation or forcing chain.
- Applies only to exponent 70 and the specific upper limit 426011000000000.
- Does not extend to other rungs, particles, or mass formulas.
- Does not replace experimental input values with RS-derived constants.
formal statement (Lean)
90private lemma phi70_lt : Constants.phi ^ (70 : ℕ) < (426011000000000 : ℝ) := by
proof body
One-line wrapper that applies rw.
91 rw [phi_eq_goldenRatio]; exact Numerics.phi_pow70_lt