pith. machine review for the scientific record. sign in
def definition def or abbrev high

mu_codata

show as:
view Lean formalization →

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.

claimLet $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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  44def mu_codata : ℝ := 1836.15267343

proof body

Definition body.

  45
  46/-! ## Predicted ratio -/
  47
  48/-- Predicted dimensionless ratio from the φ-ladder. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.