muE_deviation_upper
plain-language theorem explainer
The upper CODATA ±10σ endpoint of the muon-to-electron mass ratio satisfies R_hi^88 < φ^975, forcing the ladder deviation ε = log_φ R − 11 to obey ε < 7/88 across the whole measured window. Cited by the sigma0 mass-ratio binding bundle and by the real-side lift of the same certificate. Proof is a single kernel decide on exact arithmetic in ℤ[φ].
Claim. Writing $R_{\mathrm{hi}}$ for the upper rational endpoint of the CODATA $\pm 10\sigma$ muon/electron mass-ratio window (denominator $10^7$), one has $R_{\mathrm{hi}}^{88} < \varphi^{975}$ in the $\varphi$-integer ring. Equivalently $R_{\mathrm{hi}} < \varphi^{11+7/88}$, so the deviation $\varepsilon:=\log_\varphi R-11$ satisfies $\varepsilon<7/88$ for every ratio in the window.
background
Recognition Science places particle masses on the discrete φ-ladder (powers of the golden ratio in ℤ[φ]). The RS mass law assigns muon and electron equal charge index and rungs 13 and 2, so the pure ladder prediction for $m_\mu/m_e$ is $\varphi^{11}$. CODATA 2022 reports $m_\mu/m_e=206.7682827(46)$; this module works with the deliberately wide ±10σ integer window encoded as $[\ell,h]/s$ with scale $s=10^7$.
The local setting is sigma0 mass-ratio binding: every claim is a choice-free comparison of those integer endpoints against phiPow on ℤ[φ]. The deviation exponent is $\varepsilon:=\log_\varphi R-11$. Clearing the fractional offset $7/88$ by raising to the 88th power converts the real inequality $R<\varphi^{11+7/88}$ into the integer comparison certified here. Upstream, phiPow builds exact ladder rungs by the Fibonacci recurrence in ℤ[φ].
proof idea
One-line kernel proof: by decide. The goal is a decidable rational-vs-φ-power comparison (RatLt) of the 88th powers of the integer window endpoint and scale against phiPow 975. The decision procedure expands both sides in the PhiInt basis and checks the strict inequality by exact integer arithmetic; no analytic estimates or floating-point steps appear.
why it matters
This is the upper half of the deviation bracket that forms the third conjunct of mass_ratio_binding, the full sigma0 bundle: the CODATA window lies strictly inside $(\varphi^{11},\varphi^{12})$, has unique nearest rung gap 11, and satisfies $5/63<\varepsilon<7/88$. Downstream, MassRatioBindingReal.muE_pow88_lt lifts the certificate to reals under the measured-window hypothesis, enabling the sigma1 observation that the bracket refutes the naive identification $\varepsilon=1/(4\pi)$ (since $7/88<1/(4\pi)$ via $\pi<22/7$). It is the first empirical bite of the forced-ratio thread against the φ-ladder (T6 fixed point, mass formula on rungs).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.