proton_radius_codata
plain-language theorem explainer
The declaration supplies the CODATA 2018 proton charge radius as a real constant for use in Recognition Science calculations. Physicists investigating the proton radius puzzle cite this value when testing consistency between the phi-ladder mass formula and experimental data. It is introduced as a direct abbreviation with no additional proof steps required.
Claim. The proton charge radius satisfies $r_p = 0.8414$ fm according to the CODATA 2018 evaluation.
background
Recognition Science derives physical quantities from the J-cost functional and the Recognition Composition Law. The module sets the proton radius to the measured value to enable comparisons within the framework of independent spatial semantics and coupled axes. Upstream results confirm that voxels evolve independently and that axes are carried by distinct primitives, supporting a probe-independent radius.
proof idea
The declaration is a direct abbreviation assigning the constant value 0.8414. No lemmas are applied and no tactics are used beyond the definition itself.
why it matters
This constant feeds the leptonic_universality theorem asserting probe independence and the old_value_differs comparison showing a greater than 3% discrepancy with the larger historical value. It places the proton radius within the Recognition Science framework by fixing the scale for the phi-ladder and the eight-tick octave in three spatial dimensions. The parent results use it to confirm consistency with leptonic universality without violation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.