r_bottom
plain-language theorem explainer
The integer 21 is fixed as the RS rung index for the bottom quark on the phi-ladder. Quark-mass phenomenologists cite this constant when matching Recognition Science predictions to the PDG MS-bar value 4.18 GeV. The declaration is a direct constant assignment with no further computation.
Claim. The bottom-quark rung on the Recognition Science phi-ladder is the natural number $21$.
background
The Bottom Quark MS-bar Mass Scorecard module records the PDG 2024 central value m_b(m_b) = 4.18 GeV together with the RS assignment of rung 21 for the third-generation down-type quark. The underlying mass formula is yardstick times phi to the power (rung minus 8 plus gap(Z)) evaluated on the phi-ladder. The module imports the spin-value definition from SpinStatistics, where value(s) equals s.twice divided by 2, to identify fermions.
proof idea
One-line definition that directly binds the natural number 21 to the identifier r_bottom.
why it matters
The definition supplies the rung value required by the BottomMSBarCert structure, which certifies that the RS-predicted bottom mass lies inside the PDG band. It implements the rung assignment step of the T5 J-uniqueness and phi-ladder mass formula from the UnifiedForcingChain. No open questions are closed by this constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.