mu_relative_error
The theorem shows that the relative difference between the φ-ladder predicted proton-electron mass ratio and the CODATA 2022 value remains below 4 percent. Researchers comparing discrete ladder mass formulas to experimental constants would cite this quantitative check for the Phase 0 P0-MU row. The argument invokes the established interval bracket on the prediction, records positivity of the CODATA constant, rewrites the target inequality, and discharges both sides by linear arithmetic on the bracket bounds.
claim$|μ_{pred} - μ_{CODATA}| / μ_{CODATA} < 0.04$, where $μ_{pred}$ is the ratio of predicted proton binding energy to electron mass obtained from the φ-ladder and $μ_{CODATA}$ is the fixed experimental value 1836.15267343.
background
The module records bounds on the predicted proton-electron mass ratio μ = m_p / m_e inside the φ-ladder framework of Recognition Science. mu_codata is the constant 1836.15267343 taken from CODATA 2022. mu_pred is defined as proton_binding_pred / electron_pred, the ratio of the ladder-derived proton binding energy to the ladder-derived electron mass. The upstream theorem mu_pred_bracket supplies the concrete interval 1898 < mu_pred < 1904. These objects sit inside the local setting of Phase 0 verification for row P0-MU, where the module documentation states that the predicted ratio lies near 1901 while CODATA reads 1836.15, with the deviation attributed to the proton binding energy sitting between rungs 47 and 48.
proof idea
The proof obtains the bracket hb := mu_pred_bracket. It records positivity of mu_codata by unfolding its definition and applying norm_num. The target inequality is rewritten via div_lt_iff₀ and abs_lt. After unfolding mu_codata the two sides of the absolute-value inequality are discharged simultaneously by nlinarith applied to the lower and upper bounds from hb.
why it matters in Recognition Science
This result supplies the final numerical comparison required by the downstream theorem muRatioScoreCardCert_holds, which packages the electron bounds, proton bounds, prediction bracket, and relative-error bound into a single certificate. It completes the CODATA comparison step outlined in the module documentation for the P0-MU row. Within the Recognition framework the bound quantifies the current agreement of the φ-ladder mass formula with experiment before the next refinement pass that aligns the proton rung.
scope and limits
- Does not claim exact numerical equality with the CODATA value.
- Does not derive the absolute mass values, only their ratio.
- Does not incorporate higher-order rung corrections or binding refinements.
- Does not address the physical origin of the observed 4 percent discrepancy.
formal statement (Lean)
108theorem mu_relative_error : |mu_pred - mu_codata| / mu_codata < 0.04 := by
proof body
Tactic-mode proof.
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