top_rung_eq
plain-language theorem explainer
The declaration records that the phi-ladder rung for the top quark fermion equals 21. Researchers deriving CKM matrix structure or heavy-quark masses from the Recognition Science phi-ladder would cite this anchor. The proof is immediate reflexivity on the explicit definition of the rung map.
Claim. Let $f$ be the top quark in the fermion classification. The rung index assigned to $f$ on the phi-ladder satisfies $r(f)=21$.
background
The Quark Anchor Derivation module obtains heavy-quark masses from the RSBridge formula massAtAnchor $f = M_0 * exp(((rung f : R) - 8 + gap(ZOf f)) * log phi)$, with all quantities RS-native and dimensionless. The rung function maps each fermion species to an integer position on the phi-ladder. Upstream definitions fix the top-quark entry at 21 in the RSBridge Anchor module and in the sibling Fermion inductive type.
proof idea
One-line wrapper that applies reflexivity directly to the definition of rung on the top-quark constructor.
why it matters
The result supplies the top-rung clause inside QuarkAnchorDerivationCert and is consumed by CKMHierarchyFromPhiLadderCert, whose clauses include quark_rungs_strict_ordering and mass_geometric. It therefore anchors the heaviest quark in the phi-ladder hierarchy (T6 fixed point) used to derive the CKM structure without external mass data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.