mu_codata
plain-language theorem explainer
mu_codata records the CODATA 2022 experimental value of the proton-electron mass ratio as the real constant 1836.15267343. Researchers comparing Recognition Science phi-ladder mass predictions to laboratory data cite this constant when they quantify the relative error between the predicted ratio and the measured value. The definition is a direct numerical assignment with no lemmas or computational reduction.
Claim. Let $mu_{codata}$ denote the CODATA 2022 proton-electron mass ratio $mu = m_p/m_e$, the real number $1836.15267343$.
background
In the Recognition Science framework the proton-electron mass ratio is treated as a dimensionless observable whose experimental value is stored for direct comparison with phi-ladder predictions. The module records the CODATA figure together with proved interval bounds on the predicted electron mass near rung 59 and the binding-energy-dominated proton mass near rung 43. The upstream PrimitiveDistinction.from theorem supplies the seven-axiom foundation that justifies the structural conditions used in all mass derivations.
proof idea
The declaration is a direct definition that binds the literal real number 1836.15267343 to the identifier mu_codata. No lemmas are applied; the body consists of a single constant assignment.
why it matters
mu_codata is referenced by MuRatioScoreCardCert to certify that the predicted ratio lies in (1898,1904) and that the relative error to the experimental value is less than 4 percent. It anchors the Phase 0 scorecard comparison between the Recognition Science mass formula (yardstick times phi to the appropriate rung) and laboratory data. The open question it touches is the precise rung alignment for the proton once binding energy is fully incorporated in the ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.