phi_pow_11_approx
plain-language theorem explainer
The golden ratio raised to the eleventh power lies strictly between 198.9 and 200. Mass-comparison and lepton-ratio audits cite this certified interval to pin the raw RS muon-to-electron mass ratio at about 199. The proof multiplies certified bounds on φ⁸ and φ³, then chains the products through positivity and transitivity.
Claim. With $\varphi$ the golden ratio (Recognition Science unit scale), one has $198.9 < \varphi^{11} < 200$.
background
The MassComparison module compares Recognition Science mass predictions to PDG 2024 values. It is quarantined from the certified surface because it imports experimental numbers and uses the φ-ladder anchor system. Species masses take the form yardstick(sector) × φ^(r₀ + r_species), with coherence energy E_coh = φ⁻⁵.
Here φ is the RS constant equal to the golden ratio, forced in the foundation chain as the self-similar fixed point (T6). Certified interval lemmas in Numerics.Interval.PhiBounds already bound φ³ and φ⁸ from below and above. The present statement only needs a coarse enclosure of φ¹¹, enough to fix the sign of the raw μ/e discrepancy against experiment.
Downstream, the raw prediction discrepancy theorem records that RS predicts m_μ/m_e ≈ φ¹¹ ≈ 199 while experiment sits near 206.77 (about 4%).
proof idea
Import four certified bounds, rewritten under Constants.phi = Real.goldenRatio: 46.97 < φ⁸ < 46.99 and 4.236 < φ³ < 4.237. Factor φ¹¹ = φ⁸ · φ³ via pow_add.
Lower bound: multiply the two lower bounds with positivity of each factor (phi_pos and pow_pos), obtain 46.97 · 4.236 < φ⁸ · φ³, then norm_num shows 198.9 is strictly smaller, and lt_trans closes.
Upper bound: the same pattern with the two upper bounds yields φ⁸ · φ³ < 46.99 · 4.237 < 200. Both sides are pure real arithmetic; no floating-point tactics beyond norm_num on concrete decimals.
why it matters
Feeds the key raw_prediction_discrepancy theorem in the same module, which states that the experimental μ/e ratio exceeds φ¹¹ while the experimental τ/e ratio lies below φ¹⁷. That table is the machine-checked record that bare ladder ratios sit a few percent off PDG 2024, with the framework claiming radiative corrections close the gap.
In the broader RS picture the mass formula is yardstick × φ^(rung − 8 + gap(Z)) on the φ-ladder; φ¹¹ is exactly the rung difference that appears for the muon versus the electron. The bound is deliberately coarse: only the sign of (experiment − φ¹¹) is required, not a high-precision expansion. It therefore sits in the verification layer rather than the forcing chain (T0–T8), but it makes the lepton-ratio audit fully formal.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.