r_top
plain-language theorem explainer
The top quark rung index is set to 21 on the Recognition Science phi-ladder. Particle physicists matching RS mass predictions to the PDG top mass would reference this constant. It is introduced via direct assignment of the natural number 21.
Claim. The rung index for the top quark in the RS phi-ladder is defined by $r = 21$.
background
In the Top Quark Pole / MS-bar Mass Scorecard module, the top quark (up-type, generation 3) receives rung index 21. This supports matching the predicted MS-bar mass (approximately 162-163 GeV) to PDG 2024 data with pole mass 172.69 ± 0.30 GeV. The module exposes both pole and MS-bar forms with zero sorry or axiom.
proof idea
The declaration is a direct constant definition that sets the rung index to the natural number 21. No lemmas or tactics are applied.
why it matters
This definition supplies the rung value asserted in the TopMSBarCert structure via rung_eq_21. It implements the RS sector rung t = 21 noted in the module documentation, connecting to the mass formula yardstick * phi^(rung - 8 + gap(Z)) on the phi-ladder. The declaration supports certification of the top MS-bar mass prediction within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.