The muon-to-electron ratio, certified with integers only.
CODATA measures mμ/me = 206.7682827(46). Recognition Science places that
ratio between rungs 11 and 12 of the golden ladder: φ¹¹ = 199.005 and φ¹² = 321.997.
The Lean module MassRatioBinding certifies the placement, the uniqueness of the nearest rung, and a
deviation bracket, all by decide on exact golden-integer arithmetic. This script is an independent
witness of the same six inequalities, run on a tighter CODATA sub-interval (about ±1σ) that sits
inside Lean's ±10σ window: integer sign tests on numbers like
φ⁹⁷⁵ vs R88, no floating point anywhere in the verdict path. Six gates, all
PASS.
Window, uniqueness, bracket
Window (2 gates): the measured ratio sits strictly between φ¹¹ and φ¹². Uniqueness (2 gates): squaring shows rung 11 is strictly nearer than rung 12, so the assignment cannot flip. Bracket (2 gates): the fractional position ε between the rungs satisfies 5/63 < ε < 7/88, pinning it to about one part in 10⁷.
Any FAIL kills the Lean chain
The script's interval is a strict sub-interval of Lean's, so a Lean PASS implies a script PASS on every
gate. If this independent witness prints FAIL on any line, the corresponding Lean decide is
wrong.
ε vs 1/(4π)
The certified bracket puts ε in [0.0795256, 0.0795257]. Nearby landmarks: 1/(4π) = 0.0795775 and 1/(4π) − α² = 0.0795242. Both sit outside the certified interval. The script prints them as orientation, not as claims.
Where the ratio sits, drawn
Run it yourself
$ python3 mass_ratio_exact.py PASS window_lower phi^11 < R_lo PASS window_upper R_hi < phi^12 PASS nearest_lower phi^21 < R_lo^2 PASS nearest_upper R_hi^2 < phi^23 PASS eps_lower phi^698 < R_lo^63 PASS eps_upper R_hi^88 < phi^975 eps in [0.079525603, 0.079525698] 1/(4pi) = 0.079577472 1/(4pi) - alpha^2 = 0.079524220
Split tier, matching MassRatioBindingReal: the six integer gates
(σ₀) are THEOREM, proved by decide in Lean; that the true ratio lies in the CODATA
window (σ₁) is MEASURED, a hypothesis about the measurement, not a Lean proof. This script is an
independent numeric witness of the same six inequalities on a tighter CODATA sub-interval
([206.7682780, 206.7682874], about ±1σ) inside Lean's ±10σ window
([206.7682367, 206.7683287]). What it does NOT do: derive why the muon sits near rung 11, or make the
placement a prediction (the rung was identified from the measured value). What it does: certify, with exact
integer arithmetic on both sides, that the CODATA interval sits inside the stated φ-window with a unique
nearest rung and a 10⁻⁷-wide deviation bracket. A FAIL line would falsify the formalization, not
the measured mass ratio. The ε-vs-1/(4π) comparison is diagnostic: the certified interval excludes
both landmark values.