match_up_t
plain-language theorem explainer
The declaration verifies that the legacy rung constructor assigns rung 21 to the top quark fermion species. Researchers constructing fermion mass spectra on the phi-ladder would cite it to confirm the torsion assignment matches the anchored table for up-type quarks. The proof is a direct reflexivity check on the compute_rung definition.
Claim. The legacy rung constructor applied to the top quark fermion returns the integer 21.
background
The compute_rung definition in RungConstructor.Motif supplies a legacy assignment of rung integers to fermion species via sector and generation, using the universal torsion set {0,11,17} for all charged fermions. Its doc-comment notes that this version is correct for leptons and neutrinos but recommends compute_rung_sdgt for quarks. The target values appear in the noncomputable rung function of RSBridge.Anchor, which lists 21 explicitly for the top quark. The local module setting consists of verification theorems that the constructor reproduces tabulated rung values for fermions.
proof idea
The proof is a one-line term proof that applies reflexivity (rfl). Reflexivity succeeds immediately because compute_rung pattern-matches the top quark case to the constant 21.
why it matters
This verification supplies a base case for the mass formula yardstick * phi^(rung - 8 + gap(Z)) on the phi-ladder. It aligns the discrete rung inputs with the anchored table used in downstream mass calculations and supports the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain. The declaration belongs to the collection of match_ theorems that close the rung constructor against the RSBridge.Anchor table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.