125 ⟨{ electron_in_range := electron_mass_bounds 126 proton_in_range := proton_mass_bounds 127 mu_pred_in_range := mu_pred_bracket 128 mu_pct := mu_relative_error }⟩ 129 130/-! ## Falsifier 131 132If a deepening pass aligns the proton mass to rung 47 or to a 133gap-corrected position outside the band `(960, 980)` MeV, the 134predicted `μ_pred` band shifts and the 4 percent residual claim must 135be retracted. The lepton bound is independently theorem-grade and is 136not at risk under refinement. 137-/ 138 139end 140 141end IndisputableMonolith.Masses.MuRatioScoreCard
depends on (22)
Lean names referenced from this declaration's body.