up_mass_pos
plain-language theorem explainer
The up quark mass is shown positive under the Recognition Science mass law that assigns m = yardstick(S) φ^(r-8 + gap(Z)) to each fermion. Particle physicists auditing Standard Model spectrum consistency in this zero-parameter framework would cite the result. The proof is a direct one-line instantiation of the general positivity theorem for any valid sector-rung-Z triple.
Claim. Let $m_ {up}$ be the mass of the up quark given by the Recognition Science formula $m = y(S) φ^{r-8+g(Z)}$ with sector $S$, rung $r$, and gap function $g(Z)$ fixed by the up-quark geometry. Then $m_{up} > 0$.
background
The module states Standard Model mass predictions via the law m(particle) = yardstick(Sector) × φ^(r - 8 + gap(Z)), where yardstick, rung, and Z derive from cube geometry (D=3) and charge structure with zero free parameters. The upstream result predict_mass_pos asserts that predict_mass s r Z_val > 0 for any sector s, integer rung r, and integer Z_val; its proof unfolds the definition and invokes positivity of the yardstick together with positivity of the exponential term. Fermion masses are obtained by feeding the particle-specific sector, rung, and Z into predict_mass, so the up-quark case is the instance with those three parameters.
proof idea
One-line wrapper that applies predict_mass_pos to the sector, rung, and Z values belonging to the up quark.
why it matters
The declaration supplies the positivity check for the up quark within the complete list of Standard Model fermion verifications. It rests on the general mass-positivity theorem and the mass-law definition, thereby supporting the claim that all fermion masses lie on the positive phi-ladder. The result is consistent with the forcing-chain landmarks T8 (D=3) and the phi-scaling that fixes the rung and gap terms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.