phi11_gt
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 in Recognition Science
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.
scope and limits
- Does not derive the golden ratio from J-uniqueness or the forcing chain.
- Does not supply an upper bound on phi^11.
- Does not extend to mass predictions outside the lepton ratio check.
- Does not incorporate experimental uncertainties beyond the imported constants.
formal statement (Lean)
176private lemma phi11_gt : (198.9 : ℝ) < Constants.phi ^ (11 : ℕ) := by
proof body
Tactic-mode proof.
177 rw [phi_eq_goldenRatio]
178 have h8 := Numerics.phi_pow8_gt
179 have h3 := Numerics.phi_cubed_gt
180 have hpos : (0 : ℝ) < Real.goldenRatio ^ 8 := by positivity
181 have heq : Real.goldenRatio ^ 11 = Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by ring_nf
182 rw [heq]
183 calc (198.9 : ℝ) < (46.97 : ℝ) * (4.236 : ℝ) := by norm_num
184 _ < Real.goldenRatio ^ 8 * (4.236 : ℝ) := by nlinarith
185 _ < Real.goldenRatio ^ 8 * Real.goldenRatio ^ 3 := by nlinarith
186