MuRatioScoreCardCert

formal source

 114
 115/-! ## ScoreCard certificate -/
 116
 117structure MuRatioScoreCardCert where
 118  electron_in_range : (0.5098 : ℝ) < electron_pred ∧ electron_pred < (0.5102 : ℝ)
 119  proton_in_range : (969 : ℝ) < proton_binding_pred ∧
 120      proton_binding_pred < (970.4 : ℝ)
 121  mu_pred_in_range : (1898 : ℝ) < mu_pred ∧ mu_pred < (1904 : ℝ)
 122  mu_pct : |mu_pred - mu_codata| / mu_codata < 0.04
 123
 124theorem muRatioScoreCardCert_holds : Nonempty MuRatioScoreCardCert :=
 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