muRatioScoreCardCert_holds
plain-language theorem explainer
The declaration certifies existence of a record confirming that phi-ladder mass predictions for the electron and proton produce a ratio within 4 percent of the CODATA value. Researchers validating dimensionless constants against the Recognition Science forcing chain would cite this when checking lepton and baryon mass formulas. The proof is a direct term construction that assembles the certificate from four separate interval lemmas on the predicted masses and their ratio.
Claim. There exists a certificate such that the predicted electron mass satisfies $0.5098 < m_e^pred < 0.5102$, the predicted proton mass satisfies $969 < m_p^pred < 970.4$, the ratio $mu_pred = m_p^pred / m_e^pred$ satisfies $1898 < mu_pred < 1904$, and $|mu_pred - mu_CODATA| / mu_CODATA < 0.04$.
background
The module records interval bounds on the dimensionless proton-electron mass ratio inside the phi-ladder framework. Electron prediction uses rung 2 while proton prediction is binding-energy dominated near rungs 47-48; the ratio is formed as the quotient of these two mass expressions. The local setting is Phase 0 row P0-MU of the physical derivation plan, where the 4 percent tolerance is introduced explicitly to cover the proton's intermediate rung position.
proof idea
The proof is a term-mode construction of the certificate record. It fills the electron interval field with the electron mass bounds lemma, the proton interval field with the proton mass bounds lemma, the ratio interval field with the mu prediction bracket lemma, and the percentage deviation field with the relative error lemma.
why it matters
This theorem supplies the proved bounds and tolerance claim for the mass ratio score card, completing the Phase 0 statement in the Masses domain. It rests on the phi-ladder mass formula and the Recognition Composition Law that fixes the self-similar scaling. The residual deviation is flagged as an open question to be closed by a future rung refinement for the proton.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.