middle_pair_sum_forced
plain-language theorem explainer
Given natural numbers a b c d summing to 38 whose overlapping-pair partition sum equals 55, the middle pair b plus c equals 17. Researchers deriving the unique SDGT assignment for up-quark, lepton, and down-quark sectors cite this to fix the lepton position. The argument applies the decomposition of the partition sum into total sum plus middle pair and solves the resulting arithmetic equation.
Claim. Let $a,b,c,d$ be natural numbers. If $a+b+c+d=38$ and the partition sum $a+2b+2c+d=55$, then $b+c=17$.
background
The partition sum is defined as $a + 2b + 2c + d$, counting three overlapping consecutive pairs from the sequence $(a,b,c,d)$. Its decomposition states that this equals the element sum plus the middle pair sum. In the SDGT forcing setting the four step values sum to 38 while the partition constraint requires the weighted sum to equal $N_3 = 2D^D + 1 = 55$, isolating the middle-pair condition needed for lepton uniqueness.
proof idea
The proof invokes the decomposition theorem partition_sum a b c d = (a + b + c + d) + (b + c) and applies the omega tactic to solve the linear equation for b + c.
why it matters
This lemma supplies the middle-pair condition that feeds directly into sdgt_assignment_forced, completing the uniqueness argument for the sector assignment (up quarks {13,11}, leptons {11,6}, down quarks {6,8}). It implements the partition constraint of the SDGT forcing theorem, which rests on the requirement that three sectors partition N3 via overlapping pairs, consistent with the eight-tick octave and D=3 in the forcing chain. The four step values themselves remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.