sdgt_differs_down_b
plain-language theorem explainer
The theorem shows that the sector-dependent SDGT rung constructor assigns a different integer to the bottom quark than the legacy universal-torsion constructor. Mass-ladder modelers in Recognition Science cite it to justify the SDGT switch for quarks. The proof is a one-line decidable computation that evaluates both functions on the b-fermion and returns inequality.
Claim. Let $b$ be the bottom quark fermion. Then the sector-dependent torsion rung constructor applied to $b$ differs from the universal-torsion rung constructor applied to $b$.
background
The module supplies proofs that the rung constructor reproduces the charged lepton table. Upstream, the legacy rung constructor applies universal torsion {0,11,17} to all charged species and is stated to be correct for leptons and neutrinos. The SDGT rung constructor replaces this with sector-dependent torsion: lepton rungs are derived while quark rungs remain hypotheses fitted to PDG data. The cellular-automata step definition supplies the underlying locality rule but is not used here.
proof idea
The proof is a one-line wrapper that invokes the decidable equality checker on the pair of rung values for the bottom quark fermion.
why it matters
This result exhibits an explicit difference for the bottom quark, thereby supporting adoption of the SDGT constructor for quarks in the mass formula. It sits inside the rung-construction proofs that feed the phi-ladder mass assignments and aligns with the T5 J-uniqueness and T6 phi fixed-point steps of the forcing chain. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.