phi11_gt
plain-language theorem explainer
The lemma establishes that the golden ratio raised to the eleventh power exceeds 198.9. Researchers verifying lepton mass predictions in the Recognition Science framework cite this bound when controlling the discrepancy in the muon-electron ratio. The proof rewrites the constant to the golden ratio, decomposes the exponent as 8 plus 3, and chains the pre-established lower bounds on the eighth and third powers through numerical comparison and linear arithmetic.
Claim. $phi^{11} > 198.9$ where $phi$ denotes the golden ratio.
background
The Verification module compares Recognition Science lepton mass predictions against PDG 2024 experimental values, treating the latter as imported constants. The lepton formula takes the form $m(Lepton, r) = phi^{57+r} / (2^{22} times 10^6)$ in MeV. This lemma supplies the concrete numerical lower bound on $phi^{11}$ required for the muon rung in ratio checks.
proof idea
The tactic proof first rewrites Constants.phi to Real.goldenRatio. It obtains the bounds 46.97 < goldenRatio^8 and 4.236 < goldenRatio^3, decomposes the exponent 11 as 8 plus 3 by ring_nf, verifies the base inequality 198.9 < 46.97 * 4.236 by norm_num, and lifts the comparison to the powered terms with two nlinarith steps.
why it matters
This bound is invoked directly by the muon_electron_ratio_error theorem to establish that the relative discrepancy between the phi-based prediction and experiment remains below 0.04. It closes a numerical verification step for the phi-ladder mass formula at the muon rung. The result aligns with the eight-tick octave structure and supports the overall mass predictions in the lepton sector without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.