`mu_pred_bracket`

proved

show as: view math explainer →

module: IndisputableMonolith.Masses.MuRatioScoreCard
domain: Masses
line: 98 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Masses.MuRatioScoreCard on GitHub at line 98.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  95    exact mul_lt_mul_of_pos_left he_lo h1904
  96  linarith
  97
  98theorem mu_pred_bracket : (1898 : ℝ) < mu_pred ∧ mu_pred < (1904 : ℝ) :=
  99  ⟨mu_pred_lower, mu_pred_upper⟩
 100
 101/-! ## CODATA comparison
 102
 103The predicted ratio is approximately 1901, while CODATA reads 1836.15.
 104The relative residual `(μ_pred - μ_codata) / μ_codata` is bounded
 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 }⟩

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.