only_11_6_sum_to_17
plain-language theorem explainer
The declaration proves that among pairs from the set {13, 11, 6, 8}, only 11 and 6 sum to 17. Researchers modeling sector-dependent generation torsion cite it to place the lepton sector in the middle position of the forced ordering. The proof is a single-term exhaustive check that applies the omega decision procedure to the six arithmetic statements.
Claim. Among pairs drawn from the set $S = {13, 11, 6, 8}$, the only pair summing to 17 is ${11, 6}$, i.e., $13 + 11 ≠ 17$, $13 + 6 ≠ 17$, $13 + 8 ≠ 17$, $11 + 8 ≠ 17$, $6 + 8 ≠ 17$, and $11 + 6 = 17$.
background
The SDGT Forcing module shows that sector-dependent generation torsion is forced by three constraints: the partition constraint (three overlapping consecutive-pair spans sum to $N_3 = 2D^D + 1 = 55$), lepton uniqueness (only the middle pair sums to $W = 17$), and charge asymmetry ($|Q̃_up| ≠ |Q̃_down|$). The four step values are given as ${V+F-C, E_pass, F, V} = {13, 11, 6, 8}$. This theorem supplies the lepton-uniqueness clause by exhaustive verification that the middle pair must be ${11, 6}$. No upstream lemmas are required; the result is a direct arithmetic fact inside the module.
proof idea
The proof is a one-line term-mode wrapper. It uses refine to produce the six conjuncts and hands each to the omega tactic, which decides the integer equalities and inequalities by linear arithmetic.
why it matters
The result completes the lepton-uniqueness step inside the SDGT Forcing Theorem, which together with the partition constraint and charge asymmetry selects the unique ordering (13, 11, 6, 8) for the generation steps. It thereby advances the claim that the torsion assignment is forced rather than arbitrary. The module doc notes that the origin of the specific step values {13, 11, 6, 8} as Q₃ cell counts remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.