all_fermion_masses_pos
plain-language theorem explainer
The theorem states that the Recognition Science mass formula yields strictly positive values for each of the nine charged fermions. A physicist checking the phi-ladder predictions would cite it to confirm the base inequality before any PDG comparison. The proof is a one-line term that performs case analysis over the Fermion constructors and hands each to the general predict_mass_pos lemma.
Claim. For every fermion $f$ in the set consisting of the electron, muon, tauon, up, charm, top, down, strange, and bottom, the mass given by $m(f)=$ yardstick(Sector) $× φ^{r-8+gap(Z)}$ satisfies $m(f)>0$.
background
The module states the RS mass law $m(particle)=$ yardstick(Sector) $× φ^{r-8+gap(Z)}$ with yardstick, rung $r$, and charge gap $Z$ obtained from $D=3$ cube geometry and wallpaper groups. Fermion is the inductive type that enumerates the nine charged leptons and quarks. The upstream lemma predict_mass_pos asserts that the mass function is positive for any valid sector, rung, and $Z$ value.
proof idea
The proof is a term-mode one-liner: it introduces the fermion, performs exhaustive case analysis on its nine constructors, and applies predict_mass_pos to each case.
why it matters
This supplies the all_positive component of sm_verification_cert, which certifies the full SM mass verification. It closes the positivity step of the mass law inside the T5-T8 forcing chain, where phi-scaling and three spatial dimensions fix the ladder. It leaves open the interval-arithmetic comparison of explicit numerical predictions against experiment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.