Foundation Dimensional Bridge Structural M E Si Pos

The positive electron mass

The electron mass is a physical constant, roughly 9.109 × 10⁻³¹ kilograms or, in particle physics units, about 0.511 MeV/c². The declaration m_e_SI_pos is a formal statement inside the Recognition Science framework's machine-checked library of formal theorems. It proves, from the definition of the SI electron mass used there, that this number is greater than zero. That is, the framework's stored value for the electron mass in SI units is a positive real number.

The proof is short and direct. The library defines the SI electron mass as 0.5109989461 MeV, a value taken from the CODATA 2022 adjustment. The theorem then simply verifies that this decimal is positive, using the computer's arithmetic checker. This is not a measurement, not a derivation from deeper principles, and not a claim about the physical world beyond the definition itself. It is a sanity check: the stored constant has the sign a mass must have.

Why does such a trivial fact matter? In the framework, the SI electron mass is part of a larger structure called the dimensional bridge, which converts the framework's native units (where the speed of light is 1 and the reduced Planck constant is φ⁻⁵) into SI units. The bridge is a conversion map, and its correctness depends on the constants used being well-formed. A negative mass would break the bridge's internal consistency. The positivity theorem is one of many small checks that the bridge's inputs are valid.

The theorem does not claim that the framework has derived the electron mass from first principles. That derivation remains an open problem, explicitly labeled as the principal residual in the library. The framework's native electron mass is φ³ in coherence-energy units, a number between 4.22 and 4.24, but connecting that to the measured 0.511 MeV requires an unproven conversion factor, the cosmic-Z dressing scale. The positivity theorem merely confirms the sign of one stored constant; it says nothing about where that constant came from or why it has the value it does.

In plain terms, the declaration is a formal guarantee that the SI electron mass used in the framework is a positive number. It is a small but necessary step in the framework's attempt to relate its internal units to the familiar units of physics. The larger claim, that the electron mass can be derived from the framework's axioms, remains open, and this theorem does not advance it.

/-- `m_e_SI_MeV > 0`. -/
theorem m_e_SI_pos : 0 < m_e_SI_MeV := by unfold m_e_SI_MeV; norm_num

What this page does not claim

This answer does not claim that the framework derives the electron mass from first principles. This answer does not claim that the SI electron mass value is a measurement made by the framework. This answer does not claim that the positivity theorem has any physical content beyond the definition it checks.

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/Foundation/DimensionalBridgeStructural.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: