match_up_u
plain-language theorem explainer
The theorem verifies that the legacy rung constructor assigns rung 4 to the up quark. Researchers building phi-ladder mass spectra in Recognition Science cite these match results to confirm table reproduction for first-generation quarks. The proof reduces immediately to reflexivity on the definition of the rung function.
Claim. The legacy rung constructor returns $4$ for the up quark fermion.
background
This sits among sibling match theorems in the RungConstructor.Proofs module that verify rung assignments for leptons, quarks, and bosons. The upstream compute_rung definition implements a legacy constructor using universal torsion values {0,11,17} for charged particles; it matches on species, sector, and generation to produce an integer rung. The module doc focuses on lepton tables while the declaration targets the up quark, and the snippet notes that quarks should eventually use the sdgt variant instead.
proof idea
One-line wrapper that applies reflexivity to the match clause inside the legacy rung constructor for the up quark species.
why it matters
The result places the up quark at rung 4 on the phi-ladder, directly supporting the mass formula (yardstick times phi to the power of rung minus 8 plus gap). It belongs to the verification suite that checks reproduction of observed particle tables under the Recognition framework landmarks T5 (J-uniqueness) and the mass ladder construction. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.