bottom_rung_eq
plain-language theorem explainer
The bottom quark fermion receives rung 21 on the Recognition Science phi-ladder. Heavy-quark mass derivations cite this assignment when constructing the anchor certificate from the RSBridge formula without PDG inputs. The equality is immediate from the case definition of rung on the Fermion inductive type.
Claim. The rung number for the bottom quark $b$ satisfies rung$(b) = 21$.
background
The Heavy Quark Anchor Derivation module obtains dimensionless masses via massAtAnchor f = M0 * exp(((rung f : ℝ) - 8 + gap (ZOf f)) * log φ). The Fermion inductive type enumerates quarks and leptons, with rung a noncomputable function that maps each constructor to an integer ladder position. Upstream definitions in RSBridge.Anchor supply the explicit case | .b => 21, matching the pattern used for top at rung 21 and charm at rung 15.
proof idea
One-line wrapper that applies reflexivity to the case definition of rung on Fermion.b.
why it matters
This rung equality is assembled into quarkAnchorDerivationCert_holds, which certifies the full set of charm, bottom, and top anchors. It supplies the bottom slot in the heavy-quark phi-ladder chain, consistent with the eight-tick octave and mass formula that places bottom and top at the same rung. No open scaffolding questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.