m_e_pos
plain-language theorem explainer
The declaration proves that the Recognition Science electron mass in native units is strictly positive. Derivations of the lepton spectrum and proton-electron ratio cite this base case before scaling to higher rungs. The proof is a one-line term that unfolds the mass definition and applies the positivity tactic.
Claim. The electron mass in Recognition Science units satisfies $m_{e,rs} > 0$, where $m_{e,rs} := E_{coh} · ϕ^r$ with coherence energy $E_{coh} = ϕ^{-5}$ and lepton rung $r = 2$.
background
The module formalizes C-007, the electron mass derivation from the phi-ladder. The electron occupies rung 2 on the lepton ladder, so that $m_{e,rs} = ϕ^{-3}$ after scaling by the coherence energy $E_{coh} = ϕ^{-5}$. Upstream, the rung assignment is supplied by Anchor and the positivity of phi follows from the foundational distinction primitives. The general mass formula is the yardstick scaled by phi to the appropriate rung power.
proof idea
The proof unfolds the definition of the electron mass in RS units and invokes the positivity tactic, which succeeds on the product of the positive coherence energy and a positive power of phi.
why it matters
This positivity result is used directly in the conjunction theorem electron_mass_derived that resolves C-007. It also feeds the proton-electron mass ratio and the lepton mass ladder. Within the Recognition framework it confirms the base case of the eight-tick octave mass scaling before higher rungs are considered.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.