mu_relative_error
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.