muE_window_upper
plain-language theorem explainer
The upper CODATA ±10σ endpoint of the muon/electron mass ratio lies strictly below the twelfth φ-ladder rung (φ¹² ≈ 321.997). Cited by the sigma0 mass-ratio binding bundle and by the real-window certificate that places any windowed R between consecutive rungs. Closed by a single kernel decide on the decidable positivity witness for the rational-vs-GoldenInt comparison.
Claim. With $R_{\mathrm{hi}} = 2067683287/10^{7}$ the upper endpoint of the CODATA 2022 $\pm 10\sigma$ window for $m_\mu/m_e$, one has $R_{\mathrm{hi}} < \varphi^{12}$, where $\varphi^{12}$ is the twelfth rung of the $\varphi$-ladder in $\mathbb{Z}[\varphi]$.
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 with common scale $10^7$.
The comparison predicate RatLt asserts that a rational $p/q$ (here the upper endpoint over $10^7$) lies strictly below a GoldenInt $x$, via the decidable positivity of the integer witness $q\cdot x - p$. Powers of φ are the structural-recursion elements phiPow $n = \langle F(n-1), F(n)\rangle$ in $\mathbb{Z}[\varphi]$, which reduce under kernel decide. Level 1 of the module places the whole measured window strictly between consecutive rungs 11 and 12.
proof idea
One-line kernel proof: by decide. The goal is the decidable Prop RatLt on the concrete integers muE_hi, muE_scale and the fully reduced GoldenInt phiPow 12; the kernel evaluates the positivity witness and closes. No lemmas are invoked beyond the definitions of those three constants and the RatLt predicate.
why it matters
This is the upper half of the Level-1 window sandwich. It is conjoined with the matching lower bound inside mass_ratio_binding, the full sigma0 bundle that also packages nearest-rung uniqueness and the deviation bracket $5/63 < \varepsilon < 7/88$. Downstream, muE_window_between_rungs lifts both window certificates to the reals: any $R$ in the measured window satisfies $\varphi^{11} < R < \varphi^{12}$.
In the RS mass law the muon and electron share charge index and sit on rungs 13 and 2, so the pure φ-power prediction is $\varphi^{11}$. The window certificate shows the entire CODATA ±10σ band lies strictly above that rung and strictly below the next, which is the first arithmetic contact between the forced ladder and a measured mass ratio. Framework landmarks: φ-ladder (T6 fixed point) and the mass formula yardstick $\cdot\varphi^{(\mathrm{rung}-8+\mathrm{gap}(Z))}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.