proton_mass_MeV_pos
plain-language theorem explainer
This lemma confirms the positivity of the proton mass drawn from CODATA 2022 data. Researchers comparing Recognition Science mass predictions against experiment cite it to validate numerical bounds before further analysis. The proof reduces directly to numerical normalization on the constant definition.
Claim. Let $m_p$ denote the proton rest mass in MeV units taken from CODATA 2022. Then $0 < m_p$.
background
The ExternalAnchors module serves as the single quarantined location for all empirical calibration data entering Recognition Science. It supplies CODATA 2022 values for fundamental constants and particle masses while enforcing a mechanical separation: the cost-first core never imports this module. All definitions carry the external_anchor attribute for audit.
proof idea
One-line wrapper that applies the norm_num tactic to the definition of proton_mass_MeV, which evaluates to the positive literal 938.27208943.
why it matters
The lemma supplies a basic positivity check for the external proton-mass anchor used in calibration against RS-native constants derived from the RCL and forcing chain. It supports the clean boundary between pure derivation (T0-T8 landmarks) and empirical comparison without introducing any hypothesis structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.