old_value_differs
plain-language theorem explainer
The theorem quantifies that the older proton radius value 0.877 fm exceeds the CODATA 2018 value by more than 0.03 fm. Physicists examining the proton radius puzzle cite this numerical discrepancy to frame the tension between historical data and modern measurements. The proof is a direct numerical verification via normalization.
Claim. Let $r_p = 0.8414$ fm be the CODATA 2018 proton charge radius. Then $0.877 - r_p > 0.03$.
background
The declaration belongs to the Proton Charge Radius module, whose local setting is the derivation of the proton charge radius from Recognition Science as laid out in the paper RS_Proton_Radius_Puzzle.tex. The central abbreviation proton_radius_codata supplies the fixed CODATA 2018 value 0.8414 fm together with the statement that the radius is probe-independent, implying no leptonic universality violation.
proof idea
The proof is a one-line wrapper that applies the norm_num tactic to confirm the concrete numerical inequality 0.877 - 0.8414 > 0.03.
why it matters
The result records the >3% gap between the historical 0.877 fm value and CODATA data, thereby motivating the Recognition Science account via the phi-ladder mass formula and form-factor corrections inside the proton-radius module. It rests on the upstream reduction from seven axioms to four structural conditions plus three definitional facts and on the phi-based correction factor 1/(phi N). No downstream uses are recorded, so the statement functions as a module-level numerical anchor rather than a lemma for further theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.