bottom_mass_pos
plain-language theorem explainer
The bottom quark mass is strictly positive under the Recognition Science mass law. Particle physicists auditing Standard Model predictions in the phi-ladder framework would cite this result. The proof is a one-line wrapper that instantiates the general positivity theorem for any valid sector, rung, and Z configuration.
Claim. $0 < m_b$ where $m_b :=$ yardstick(fermionSector(bottom)) $×$ $φ^{r-8+gap(Z)}$ with $r$ and $Z$ the rung and charge index for the bottom fermion.
background
The module states the mass law $m(particle) = $ yardstick(Sector) $×$ $φ^{r-8+gap(Z)}$ with yardstick, rung, and gap derived from cube geometry ($D=3$) and charge structure, zero free parameters. fermionMass(f) is the definition that selects fermionSector(f), fermionRung(f), and fermionZ(f) to compute this expression for any fermion f. The upstream theorem predict_mass_pos asserts that predict_mass s r Z_val > 0 for every valid configuration.
proof idea
One-line wrapper that applies predict_mass_pos to the sector, rung, and Z values of the bottom fermion.
why it matters
This theorem completes the positivity proof for the bottom quark in the full Standard Model fermion set. It supports the mass-law verification step in the Recognition Science chain, where masses sit on the phi-ladder with the eight-tick octave and D=3. The result feeds the module's claim that all fermion masses are positive before numerical PDG comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.