middle_pair_is_11_6
plain-language theorem explainer
The theorem shows that any distinct pair from the set {13, 11, 6, 8} summing to 17 must be exactly 11 and 6 in either order. Researchers deriving the forced lepton sector placement in sector-dependent generation torsion cite this result. The argument expands finite-set membership via simplification and resolves the remaining arithmetic cases directly.
Claim. Let $S = {13, 11, 6, 8}$. If $b, c$ are natural numbers with $b + c = 17$, $b, c ∈ S$, and $b ≠ c$, then $(b = 11 ∧ c = 6) ∨ (b = 6 ∧ c = 11)$.
background
The SDGT Forcing Theorem establishes that sector-dependent generation torsion is forced by three constraints: the partition constraint requiring three overlapping consecutive-pair spans to sum to N₃ = 2D^D + 1 = 55, lepton uniqueness requiring only the pair summing to W = 17 to occupy the middle position, and charge asymmetry requiring unequal end spans. The four step values are given as {V+F-C, E_pass, F, V} = {13, 11, 6, 8}. Lepton uniqueness isolates the middle pair as the unique pair from this set that sums to 17.
proof idea
The proof is a one-line wrapper that applies simp to expand the Finset membership conditions for the four-element set, then invokes omega to discharge the resulting finite arithmetic disjunctions.
why it matters
This result supplies the lepton uniqueness step inside the SDGT Forcing Theorem, which combines with the partition constraint and charge asymmetry to select the unique assignment: up quarks {13, 11}, leptons {11, 6}, down quarks {6, 8}. It thereby closes one of the three forcing conditions listed in the module. The four step values themselves remain open for derivation from a single principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.