MuRatioScoreCardCert
The MuRatioScoreCardCert structure records four numerical bounds on the phi-ladder predictions for the electron mass, proton binding mass, their ratio, and the relative deviation from the CODATA proton-electron mass ratio. Researchers comparing Recognition Science mass ladders to experiment would cite this certificate to document the current 4 percent agreement level. It is assembled as a plain structure definition from the already-established interval theorems for the electron mass, proton mass, the derived ratio bracket, and the relative 4% 4
claimLet $m_e^pred$ and $m_p^pred$ denote the predicted electron and proton-binding masses in MeV from the phi-ladder. Let $mu_pred = m_p^pred / m_e^pred$ and let $mu_CODATA = 1836.15267343$. The certificate asserts $0.5098 < m_e^pred < 0.5102$, $969 < m_p^pred < 970.4$, $1898 < mu_pred < 1904$, and $|mu_pred - mu_CODATA| / mu_CODATA < 0.04$.
background
In the Recognition Science framework the proton-electron mass ratio is predicted from the phi-ladder. The electron mass is obtained as phi^59 / 2^22 / 10^6 MeV while the proton binding contribution is phi^43 / 10^6 MeV. Their ratio is therefore defined by division of these two expressions. The module also imports the CODATA value 1836.15267343 as the reference ratio. The certificate packages the interval statements that have already been proved for the individual masses and for the derived ratio, together with a relative-error bound. Upstream results supply the explicit definitions of the predicted electron and proton masses in terms of Constants.phi together with the positivity lemmas needed to manipulate the inequalities.
proof idea
MuRatioScoreCardCert is a structure definition whose four fields are simply the statements of the four bounds. No proof is attached to the structure itself; the fields are populated later by the theorem that witnesses the certificate is inhabited, using the lemmas electron_mass_bounds, proton_mass_bounds, mu_pred_bracket and mu_relative_error.
why it matters in Recognition Science
This certificate closes the Phase 0 row P0-MU of the physical derivation plan by exhibiting a concrete numerical comparison between the phi-ladder mass predictions and the experimental CODATA ratio. It is used by the downstream theorem muRatioScoreCardCert_holds to witness that the certificate is inhabited. The 4 percent tolerance reflects the fact that the proton sits between phi-ladder rungs 47 and 48; a future refinement of the binding-energy term is expected to tighten the match. The construction sits inside the broader forcing chain that derives the phi self-similarity and the mass formula yardstick * phi^(rung - 8 + gap(Z)).
scope and limits
- Does not assert that the predicted ratio equals the CODATA value exactly.
- Does not derive the exponents 59 and 43 from the forcing chain.
- Does not include higher-order corrections to the proton mass.
- Does not address the fine-structure constant or other constants.
formal statement (Lean)
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