step_sum_eq
plain-language theorem explainer
The theorem confirms that the sum of the four sector step values 13, 11, 6, and 8 equals 38. Researchers modeling sector-dependent generation torsion cite this arithmetic identity when verifying the base total ahead of the partition constraint in the SDGT forcing theorem. The proof reduces directly to native computation of the integer sum.
Claim. Let $s = 13 + 11 + 6 + 8$. Then $s = 38$.
background
The SDGT Forcing module shows that sector-dependent generation torsion is forced by three constraints: the partition sum of three overlapping consecutive pairs equals 55, lepton uniqueness requires the middle pair to be 11 and 6, and charge asymmetry selects the unique ordering of the four step values. The step values 13, 11, 6, 8 are the Q3 cell counts verified in the companion SectorDependentTorsion file; step_sum is defined directly as their total. Upstream results supply the definition of step_sum together with structural facts on forcing from primitive distinctions and self-reference.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the arithmetic expression 13 + 11 + 6 + 8.
why it matters
This identity supports the SDGT Forcing Theorem by confirming the total step count before the partition constraint of 55 and the uniqueness conditions that fix the ordering (13, 11, 6, 8). It touches the open question noted in the module documentation: the specific counts are verified as Q3 cell counts but are not yet derived from a single principle. The result sits inside the masses domain and connects to the broader forcing chain without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.