electron_mass_kg
plain-language theorem explainer
The declaration supplies the CODATA 2022 numerical value for the electron rest mass in kilograms as a real constant. Researchers comparing Recognition Science mass formulas on the phi-ladder to laboratory data cite this anchor for calibration. It enters as a direct numerical assignment with no internal derivation.
Claim. The electron rest mass is defined by the numerical value $m_e = 9.1093837139(28) × 10^{-31}$ kg.
background
The module ExternalAnchors serves as the single quarantined location for all empirical calibration data entering Recognition Science from external sources. The cost-first core derives everything from the Recognition Composition Law and must not import this module, creating a mechanical separation between pure cost derivation and experimental comparison. All definitions here carry the external_anchor tag for audit purposes and use CODATA 2022 values under the SI 2019 redefinition.
proof idea
The definition is a direct numerical assignment of the real number 9.1093837139e-31 with no lemmas or tactics applied.
why it matters
This anchor supplies the measured electron mass needed to test Recognition Science mass formulas against experiment. It supports calibration of the phi-ladder and constants such as G and alpha while keeping the core RCL derivation independent of external data. The module policy enforces the separation required for the framework's claim that all physics follows from the single functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.