sdgt_differs_up_c
plain-language theorem explainer
The theorem shows that the sector-dependent SDGT rung for the charm quark differs from the legacy universal-torsion rung. Quark-mass modelers using the phi-ladder would cite it to justify switching constructors when moving from leptons to quarks. The proof reduces the inequality to a decidable equality check on the two explicit integer outputs.
Claim. Let $r_{SDGT}$ be the rung returned by the sector-dependent torsion constructor and $r_{legacy}$ the rung from the universal torsion constructor. Then $r_{SDGT}$(charm quark) differs from $r_{legacy}$(charm quark).
background
The module supplies proofs that rung construction reproduces the charged-lepton table. Legacy construction applies the same torsion triple {0,11,17} to every charged fermion and matches leptons and neutrinos exactly. SDGT construction replaces that triple with sector-dependent terms ell_baseline(sector) + tau_sdgt(sector, generation) and is required for quarks. Upstream, the legacy definition matches species to sector and generation index; the SDGT definition inserts the additional tau_sdgt correction drawn from PDG data for quarks.
proof idea
One-line wrapper that applies the decide tactic to the concrete inequality between the two rung functions evaluated at the charm fermion.
why it matters
The result isolates the point at which the legacy constructor must be replaced by the SDGT version, thereby protecting the phi-ladder mass formula yardstick * phi^(rung-8+gap(Z)) when it is applied to up-type quarks. It directly supports the framework claim that lepton rungs are derived while quark rungs remain a hypothesis pending first-principles derivation from the Recognition Composition Law. No downstream theorems are listed, leaving open the question of closing the quark-rung gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.