muon_mass_pos
plain-language theorem explainer
The muon mass prediction under the Recognition Science mass law is strictly positive. Researchers auditing zero-parameter formulas for Standard Model fermions would cite this when confirming sign consistency across the lepton sector. The proof is a direct one-line wrapper that instantiates the general positivity result for any valid sector, rung, and Z inputs.
Claim. The predicted muon mass satisfies $0 < m_μ$, where $m = y · φ^{r-8+g}$ with $y$ the yardstick of the fermion sector, $r$ the rung index, and $g$ the gap determined by charge $Z$.
background
Recognition Science assigns masses via the formula $m(particle) = $ yardstick(Sector) × φ^(rung - 8 + gap(Z)), with yardstick fixed by cube geometry in three dimensions and no free parameters. The definition fermionMass applies this expression to any fermion by supplying its sector, rung, and Z-value. The upstream theorem predict_mass_pos states that the resulting mass expression is positive for every valid integer configuration of sector, rung, and Z.
proof idea
This is a one-line wrapper that applies predict_mass_pos to the sector, rung, and Z parameters belonging to the muon.
why it matters
The declaration forms part of the Standard Model mass verification module, which records that all fermion masses remain positive under the Recognition Science law. It supports the broader claim that the phi-ladder scaling (derived from the eight-tick octave and D = 3 geometry) yields positive masses for every Standard Model particle. No open questions or scaffolding are closed by this specific result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.