phi11_lt
plain-language theorem explainer
The lemma establishes that the golden ratio raised to the eleventh power is strictly less than 200. Researchers verifying Recognition Science lepton mass predictions against PDG data cite it when bounding the muon-to-electron ratio. The proof reduces the exponent via ring algebra then chains pre-proven numerical bounds on the eighth and cubed powers through nlinarith and norm_num.
Claim. $phi^{11} < 200$ where $phi$ denotes the golden ratio.
background
The Masses.Verification module compares RS lepton mass predictions to PDG 2024 experimental values. The mass formula for the lepton sector with B_pow = -22 and r0 = 62 reads m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6) in MeV. The constant phi is identified with the golden ratio by the upstream lemma phi_eq_goldenRatio, which states Constants.phi equals Real.goldenRatio. The supporting bounds phi_pow8_lt (goldenRatio^8 < 46.99) and phi_cubed_lt (goldenRatio^3 < 4.237) are imported from the Numerics.Interval.PhiBounds module.
proof idea
The proof rewrites Constants.phi to Real.goldenRatio via phi_eq_goldenRatio. It pulls in phi_pow8_lt and phi_cubed_lt, splits the exponent with ring_nf as 11 = 8 + 3, then applies nlinarith to multiply the numerical bounds and norm_num to reach the target 200.
why it matters
This bound feeds directly into muon_ratio_undershoot and muon_electron_ratio_error, which together confirm that the RS prediction phi^11 lies below the experimental muon-electron ratio within a 4 percent error. It supports the machine-verified comparison of the lepton mass formula against PDG data. The result rests on the self-similar fixed-point property of phi (T6) and the eight-tick octave structure in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.