sdgt_differs_up_t
The theorem establishes that the sector-dependent SDGT rung constructor assigns a different integer rung to the top quark than the legacy universal-torsion constructor. Modelers of the phi-ladder mass spectrum in Recognition Science cite it to justify retaining the legacy version for leptons while adopting SDGT for quarks. The proof is a one-line decidable evaluation that computes both rung functions on the top fermion species and confirms inequality.
claimLet $r_0(t)$ denote the rung assigned to the top quark by the legacy universal-torsion constructor and $r_1(t)$ the rung from the sector-dependent torsion constructor. Then $r_1(t) ≠ r_0(t)$.
background
The legacy rung constructor applies a universal torsion set {0,11,17} to every charged fermion species. Its doc-comment states it is correct for leptons and neutrinos but requires replacement by the SDGT version for quarks. The SDGT constructor instead uses sector-dependent torsion via ell_baseline on the sector plus tau_sdgt scaled by generation index. The module supplies proofs that the rung constructor reproduces the charged lepton table, with this declaration isolating the top-quark case where the two constructors diverge.
proof idea
The proof is a one-line wrapper that applies the decide tactic. This evaluates the two rung functions on the top fermion species, reduces the inequality to a decidable integer comparison, and returns true.
why it matters in Recognition Science
The result marks the boundary between the legacy constructor (valid for leptons) and the SDGT constructor required for quarks in the mass formula yardstick * phi^(rung - 8 + gap(Z)). It supports the hypothesis that quark rungs are taken from PDG data via sector-dependent torsion while lepton rungs remain derived. No downstream theorems yet reference it, but it closes the gap between universal and sector-dependent torsion models inside the phi-ladder construction.
scope and limits
- Does not compute numerical mass values or phi-powers.
- Does not prove the SDGT rung is the physically correct choice.
- Does not apply to leptons or first- and second-generation quarks.
- Does not invoke the Recognition Composition Law or J-cost.
formal statement (Lean)
113theorem sdgt_differs_up_t : compute_rung_sdgt (.fermion .t) ≠ compute_rung (.fermion .t) := by
proof body
Decided by rfl or decide.
114 decide