mu_relative_error

formal source

 105above by 4 percent.
 106-/
 107
 108theorem mu_relative_error : |mu_pred - mu_codata| / mu_codata < 0.04 := by
 109  have hb := mu_pred_bracket
 110  have hcodata_pos : (0 : ℝ) < mu_codata := by unfold mu_codata; norm_num
 111  rw [div_lt_iff₀ hcodata_pos, abs_lt]
 112  unfold mu_codata
 113  constructor <;> nlinarith [hb.1, hb.2]
 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