leptonic_universality
plain-language theorem explainer
Physicists resolving the proton radius puzzle cite this result to confirm that the charge radius equals the CODATA 2018 value of 0.8414 fm with no dependence on the lepton probe. The declaration rules out leptonic universality violation inside the Recognition Science model. Its proof is a one-line term that witnesses the existential quantifier and closes by reflexivity.
Claim. $r_p = 0.8414$ fm (CODATA 2018), where this fixed real number is independent of the lepton species used to measure the proton charge radius.
background
The ProtonRadius module extracts the proton charge radius from Recognition Science, following the paper RS_Proton_Radius_Puzzle.tex. The central abbreviation proton_radius_codata fixes the numerical value at 0.8414 fm taken from the CODATA 2018 compilation. Upstream, the theorem from PrimitiveDistinction converts seven independent axioms into four structural conditions plus three definitional facts. The spin value definition in SpinStatistics returns twice the spin integer divided by two as a real number.
proof idea
The term proof supplies the witness for the existential quantifier directly from the codata abbreviation and closes the equality by reflexivity.
why it matters
The result places the RS proton radius on equal footing with the experimental CODATA value, thereby closing one consistency check in the proton radius puzzle. It rests on the structural conditions extracted by PrimitiveDistinction.from and on the spin-statistics definition. The declaration supports the overall derivation in RS_Proton_Radius_Puzzle.tex without invoking the phi-ladder or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.