match_down_s
plain-language theorem explainer
The theorem establishes that the legacy rung constructor assigns rung 15 to the strange quark fermion. Researchers modeling the phi-ladder mass spectrum would cite this to confirm the strange quark placement. The proof reduces immediately by reflexivity to the definition of compute_rung.
Claim. The legacy rung constructor applied to the strange quark species evaluates to the integer 15.
background
The compute_rung function is defined in the Motif module as a legacy constructor that matches on Species, using sector and generation to assign rungs via universal torsion values {0,11,17} for charged fermions. It is documented as correct for leptons and neutrinos, with a separate sdgt variant recommended for quarks. This theorem sits in the Proofs module whose module documentation states it verifies that the rung constructor reproduces the charged lepton table, though the specific instance here addresses the strange quark.
proof idea
The proof is a one-line wrapper that applies the reflexivity tactic directly to the compute_rung definition for the strange quark case.
why it matters
This declaration verifies the rung assignment for the strange quark within the legacy constructor, supporting the mass formula yardstick * phi^(rung - 8 + gap(Z)) on the phi-ladder. It fills a verification step for the particle spectrum in the Recognition Science framework, consistent with T5 J-uniqueness and the eight-tick octave. No parent theorems are listed in the used-by edges.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.