down_mass_pos
plain-language theorem explainer
The down fermion mass is positive because the general positivity result for any predicted mass applies directly to the down configuration's sector, rung, and Z. Researchers auditing Recognition Science mass predictions for Standard Model fermions would cite this when confirming the full set of quark and lepton masses. The proof is a one-line wrapper that invokes predict_mass_pos on the down parameters.
Claim. The predicted mass of the down quark satisfies $0 < m$, where $m = $ yardstick(sector) $× φ^{r-8 + gap(Z)}$ and the sector, rung $r$, and $Z$ are those assigned to the down fermion.
background
The Standard Model Mass Verification module states the mass law $m(particle) = $ yardstick(Sector) $× φ^{r-8 + gap(Z)}$ with parameters fixed by cube geometry in three dimensions and wallpaper groups, carrying zero free parameters. The sibling definition fermionMass extracts the required sector, rung, and Z for any Fermion and feeds them into predict_mass. The upstream theorem predict_mass_pos shows that this expression is always positive by unfolding to a product of positive terms, beginning with the yardstick being positive.
proof idea
One-line wrapper that applies predict_mass_pos to the down fermion by supplying its sector, rung, and Z values through the fermionMass definition.
why it matters
This declaration belongs to the family of fermion mass positivity results that together confirm the mass law produces positive values for all Standard Model particles. It supports the module's claim that mass law positivity is proved while PDG comparisons remain hypotheses. The result sits inside the Recognition Science mass formula that uses the phi-ladder, D=3, and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.