match_rsbridge_rung_up_quarks
plain-language theorem explainer
The declaration verifies that the legacy rung constructor yields the same integer assignments as the RSBridge anchor mapping for the up-type quarks u, c, and t. Mass modelers building phi-ladder spectra would cite it to confirm that the Motif implementation preserves the prior fermion rung table. The proof is a direct reflexivity check on the three equalities.
Claim. Let $C$ be the legacy rung constructor on fermion species and $R$ the RSBridge anchor mapping. Then $C(u) = R(u)$, $C(c) = R(c)$, and $C(t) = R(t)$.
background
The rung constructor appears in the Motif module as a legacy function assigning universal torsion values from the set {0,11,17} for all charged fermions. Its documentation states it is correct for leptons and neutrinos but recommends compute_rung_sdgt for quarks. The RSBridge anchor supplies the explicit integer table: 4 for u, 15 for c, and 21 for t. This theorem belongs to the proofs module whose module documentation describes verification that the rung constructor reproduces charged lepton tables, with sibling theorems handling leptons, down quarks, and bosons. Upstream results include the rung definition in AnchorPolicy that routes up quarks to the integer ladder and the constant rung value 1 in Compat.Constants.
proof idea
The proof is a one-line wrapper that applies reflexivity to each of the three conjuncts.
why it matters
The result closes a consistency check between the Motif constructor and the legacy RSBridge anchor, supporting the mass formula that places particles on the phi-ladder via rung minus 8 plus gap(Z). It aligns with the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain and with the eight-tick octave. No direct downstream theorems are recorded, yet the verification is required before the constructor can be used in full mass computations or in the Recognition Composition Law applications.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.