muE_deviation_lower
plain-language theorem explainer
The lower CODATA ±10σ endpoint of the muon–electron mass ratio obeys φ^698 < R_lo^63, i.e. R_lo > φ^(11 + 5/63). Anyone citing the forced deviation bracket ε > 5/63 for m_μ/m_e against the φ-ladder needs this certificate. The proof is a single kernel decide on the decidable integer predicate RatGt over ℤ[φ].
Claim. Let $R_{\mathrm{lo}} = 2067682367/10^7$ be the lower endpoint of the CODATA 2022 $\pm 10\sigma$ window for $m_\mu/m_e$. Then $\varphi^{698} < R_{\mathrm{lo}}^{63}$, equivalently $\varphi^{11+5/63} < R_{\mathrm{lo}}$. Writing $\varepsilon := \log_\varphi R - 11$ for the deviation from rung 11, one has $\varepsilon > 5/63$ throughout the window.
background
MassRatioBinding is the first empirical bite of the forced-ratio thread: a measured particle-mass ratio is bound against φ-ladder rungs by choice-free integer arithmetic alone. CODATA 2022 quotes $m_\mu/m_e = 206.7682827(46)$; the module works with the generous ±10σ window $R \in [206.7682367, 206.7683287]$, encoded exactly as the integer interval $[\mathrm{muE_lo}, \mathrm{muE_hi}]/\mathrm{muE_scale}$ with scale $10^7$.
The φ-ladder is the sequence $\varphi^n \in \mathbb{Z}[\varphi]$, built here by structural recursion so that comparisons reduce under decide. The predicate RatGt $p$ $q$ $x$ asserts that the rational $p/q$ lies strictly above the GoldenInt $x$, decided by positivity of an integer witness. Three binding levels are proved: the window sits between rungs 11 and 12; 11 is the unique nearest integer rung gap; and the deviation $\varepsilon = \log_\varphi R - 11$ is bracketed by rationals.
This declaration is the lower half of level 3. The RS mass law assigns muon and electron equal charge index and rungs 13 and 2, predicting the pure power $\varphi^{11}$; the measured window brackets that gap and forces a small positive $\varepsilon$.
proof idea
One-line kernel decision. After unfolding RatGt, muE_lo, muE_scale, and the recursive phiPow, the goal is a concrete positivity statement in ℤ[φ] (equivalently a sign check on a Fibonacci-coefficient integer). The Decidable instance for RatGt discharges it by decide inside the trusted kernel; no lemmas beyond the definitions are invoked.
why it matters
This is one conjunct of the full sigma0 bundle mass_ratio_binding, which packages window, nearest-rung, and deviation certificates as a single choice-free fact on ℤ[φ]. Downstream, MassRatioBindingReal.muE_pow63_gt lifts the certificate to reals: under the hypothesis that $R$ lies in the CODATA window, $\varphi^{698} < R^{63}$.
Together with the matching upper bound $R_{\mathrm{hi}}^{88} < \varphi^{975}$, one obtains the tight rational bracket $5/63 < \varepsilon < 7/88$ (numerically $0.079365 < \varepsilon < 0.079545$). Since $7/88 < 1/(4\pi)$ (via $\pi < 22/7$), the bracket refutes the naive identification $\varepsilon = 1/(4\pi)$ at ≥10σ. In the broader RS picture this is the first place a measured mass ratio is pinned to the φ-ladder (primer mass formula, rung gap 11) by pure integer arithmetic, with the physical-window claim kept as an explicit sigma1 hypothesis rather than a theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.