sdgt_differs_down_s
plain-language theorem explainer
The theorem shows that the sector-dependent rung constructor assigns a different integer to the strange quark than the legacy universal-torsion constructor. Mass-ladder builders in Recognition Science cite it when switching constructors for down-type quarks. The proof reduces to a single decidable equality test on the two integer outputs.
Claim. Let $r_0$ be the legacy rung constructor and $r_1$ the sector-dependent rung constructor. Then $r_1(s) ≠ r_0(s)$ where $s$ denotes the strange quark.
background
The module supplies proofs that rung constructors reproduce particle tables. The legacy constructor applies the same torsion triple {0,11,17} to every charged fermion. The sector-dependent constructor replaces this with ell_baseline plus a generation-dependent tau_sdgt term that varies by lepton or quark sector. Upstream documentation states the legacy version is correct only for leptons and neutrinos; quarks require the sector-dependent version.
proof idea
The proof is a one-line wrapper that applies the decidable equality checker to the integer values returned by the two rung constructors on the strange-quark species.
why it matters
The result isolates the mismatch for the strange quark and thereby justifies the sector-dependent constructor for all down-type quarks inside the mass-ladder construction. It belongs to the same proof suite that verifies reproduction of the charged-lepton table, while highlighting the quark-specific adjustment. In the broader framework the rung values feed the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.