tauon_mass_pos
plain-language theorem explainer
The positivity of the RS-predicted tauon mass follows from the general mass positivity theorem applied to the tauon fermion parameters. Particle physicists auditing Recognition Science mass predictions would cite this to confirm the model yields no negative masses for any Standard Model fermion. The proof is a one-line wrapper that invokes predict_mass_pos on the tauon-specific sector, rung, and Z values.
Claim. $0 < m_τ$, where $m_τ$ is the RS mass $m = $ yardstick(Sector) $× φ^{r-8 + gap(Z)}$ evaluated at the tauon sector, rung, and charge parameters.
background
The Standard Model Mass Verification module states the mass law as $m(particle) = $ yardstick(Sector) $× φ^{r-8 + gap(Z)}$, with yardstick, rung $r$, and $Z$ drawn from cube geometry ($D=3$), wallpaper groups, and charge structure. The fermionMass definition computes this formula for each Fermion type by extracting fermionSector, fermionRung, and fermionZ. Upstream, predict_mass_pos proves that predict_mass $s$ $r$ $Z_val > 0$ for any valid configuration by unfolding to the product of a positive yardstick and a positive power of $φ$.
proof idea
One-line wrapper that applies predict_mass_pos to the sector, rung, and Z values supplied by fermionMass for the tauon.
why it matters
This result completes the positivity check for the tauon within the full set of fermion mass statements in the SMVerification module. It rests on the mass law positivity proved in MassLaw and supports the framework claim that all RS masses on the phi-ladder are positive with zero free parameters. The declaration aligns with the T5 J-uniqueness and T6 phi fixed-point steps that generate the mass scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.