strange_mass_pos
plain-language theorem explainer
The theorem establishes that the predicted mass of the strange quark is strictly positive. Researchers verifying Standard Model mass predictions within the Recognition Science framework would cite this result when confirming the mass law for fermions. The proof is a direct one-line wrapper that invokes the general positivity result for the mass prediction function.
Claim. The predicted mass of the strange quark satisfies $m > 0$, where $m$ is obtained from the mass law $m = y(S) · φ^{r-8 + g(Z)}$ with $S$, $r$, and $Z$ the sector, rung, and charge gap specific to the strange quark.
background
The mass law states that any particle mass is given by $m = $ yardstick(Sector) × φ^(r - 8 + gap(Z)), with yardstick, rung, and Z derived from cube geometry in three dimensions, wallpaper groups, and charge structure. This module states the Recognition Science mass predictions for all Standard Model particles and records their comparison with PDG 2024 values. The upstream theorem predict_mass_pos asserts that the mass is positive for any valid sector, rung, and Z configuration. The fermionMass definition computes the mass for a given fermion by supplying its sector, rung, and Z to the mass prediction function.
proof idea
The proof is a one-line wrapper that applies the general positivity theorem predict_mass_pos to the sector, rung, and Z values of the strange fermion.
why it matters
This result forms part of the module's demonstration that all fermion masses are positive. It supports the proved positivity and φ-scaling properties of the mass law, consistent with the eight-tick octave and D = 3 spatial dimensions. The declaration closes one case in the systematic verification of Standard Model masses under the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.