electron_mass_pos
plain-language theorem explainer
The electron mass is positive because the Recognition Science mass formula yields a strictly positive value for any valid sector, rung, and Z assignment. Particle physicists auditing phi-ladder predictions for the Standard Model spectrum would cite this result when confirming the lightest charged lepton. The proof is a one-line wrapper that invokes the general mass-positivity theorem on the electron parameters.
Claim. The electron mass $m_e = y(S) · φ^{r-8+g(Z)}$ satisfies $m_e > 0$, where $y(S)$ is the sector yardstick, $r$ the rung, and $g(Z)$ the gap function of the electron's charge structure.
background
The Standard Model Mass Verification module states the mass law as $m(particle) = yardstick(Sector) × φ^(r - 8 + gap(Z))$, with yardstick, rung, and Z obtained from cube geometry in three dimensions and the 17 wallpaper groups. The upstream theorem predict_mass_pos asserts that this expression is positive for every valid configuration. The fermionMass definition specializes the general formula by supplying the sector, rung, and Z values belonging to each fermion species.
proof idea
One-line wrapper that applies predict_mass_pos to the electron's sector, rung, and Z values.
why it matters
This result confirms positivity of the lightest charged lepton under the parameter-free mass law derived from the phi-ladder and D=3 geometry. It forms part of the verified positivity statements for all fermions in the Standard Model verification section. The declaration relies on the upstream mass-positivity theorem and supports downstream numerical comparisons with PDG values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.