Constants External Anchors Proton Mass Me V Pos

The proton mass anchor

The proton is one of the particles that make up atomic nuclei, and its mass is a measured fact of nature. The CODATA 2022 adjustment, the standard international compilation of physical constants, gives the proton mass as 938.27208943 MeV, where MeV is a unit of energy commonly used in particle physics. In the Recognition Science framework's machine-checked library of formal theorems, this value appears as a definition named proton_mass_MeV. The declaration proton_mass_MeV_pos is a separate lemma, a proved statement, that establishes a simple property of that definition: the number 938.27208943 is greater than zero.

That positivity lemma is a trivial mathematical fact, but it is part of a deliberate design. The library quarantines all empirical calibration data in one module, the ExternalAnchors file, so that the cost-first core of Recognition Science never imports external measurements. The proton mass is not derived from the framework's first principles; it is an external anchor, a number brought in from experiment to enable comparison with reality. The lemma proton_mass_MeV_pos does not make the mass a theorem of the framework. It only records that the anchored value is positive, a necessary sanity check for any physical mass.

What the declaration does not claim is more important than what it proves. It does not claim that Recognition Science predicts or derives the proton mass from its cost function. It does not claim the value is exact; the CODATA 2022 central value carries an uncertainty, and the library stores separate bounds for related ratios. It does not claim the proton is fundamental; the mass is simply a measured input, not an output of the framework's derivation chain. The lemma is a bookkeeping fact about an external number, not a physical law.

For a reader, the practical consequence is clarity about provenance. When a framework page cites proton_mass_MeV_pos, it is saying: this library has recorded the measured proton mass and checked it is positive. The proof is a formality, but the quarantine is the real content. It tells you where the number came from, and it tells you the framework does not pretend to have produced it from nothing.

lemma proton_mass_MeV_pos : 0 < proton_mass_MeV := by norm_num [proton_mass_MeV]

/-- **EXTERNAL ANCHOR**: Proton mass (CODATA 2022).
    m_p = 938.27208943(29) MeV/c² -/
@[simp]
noncomputable def proton_mass_MeV : ℝ := 938.27208943

/-- **EXTERNAL ANCHOR** marker type for documentation.
    This doesn't affect code but signals calibration dependence. -/
abbrev ExternalAnchorMarker := Unit

What this page does not claim

The proton mass is not derived from Recognition Science first principles. The CODATA 2022 value is not exact and carries a measurement uncertainty. The positivity lemma does not imply the proton is a fundamental particle.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Constants/ExternalAnchors.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: