electron_mass_MeV_pos
plain-language theorem explainer
The lemma establishes strict positivity of the electron rest energy in MeV units. Modelers comparing Recognition Science constants to particle data cite it to confirm the anchor lies in the physical domain. The proof reduces the inequality by a single norm_num application on the explicit decimal definition.
Claim. $0 < m_e$ where $m_e = 0.51099895069$ is the CODATA electron rest energy in MeV$/c^2$.
background
The ExternalAnchors module is the single quarantined location for all empirical calibration data entering Recognition Science. Its policy keeps the cost-first core (RCL derivations) free of external numbers while allowing comparison modules to import CODATA values under the external_anchor attribute. The upstream definition supplies the concrete real number electron_mass_MeV := 0.51099895069 to which the inequality applies.
proof idea
The proof is a one-line wrapper that invokes norm_num on the constant electron_mass_MeV, reducing the strict inequality directly to a numerical fact.
why it matters
The lemma supplies a basic sanity check on the electron-mass external anchor before it enters any downstream constant calculations. It supports safe use of the value when contrasting RS-native predictions (phi-ladder masses, alpha band) against experiment. No parent theorem or open question is attached; the result follows immediately from the numerical definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.