partition_sum_decomp
plain-language theorem explainer
The algebraic identity decomposes the partition sum of four natural numbers into their element sum plus the middle pair sum. Mass spectrum derivations in Recognition Science cite this when enforcing the partition constraint N₃ = 55 on sector steps. The proof reduces directly by unfolding the definition of the partition sum and applying arithmetic normalization.
Claim. Let $p(a,b,c,d) = a + 2b + 2c + d$. Then $p(a,b,c,d) = (a + b + c + d) + (b + c)$.
background
In the SDGT Forcing module the partition sum is defined as the sum of three overlapping consecutive-pair spans from four step values: $a + 2b + 2c + d$. This encodes the requirement that three sectors partition N₃ = 2D^D + 1 = 55, where D = 3 follows from the eight-tick octave. The element sum a + b + c + d is fixed at 38 in the downstream application, while W = 17 is the wallpaper-group count that must appear as the middle pair under lepton uniqueness.
proof idea
The proof is a one-line term-mode reduction. It unfolds the definition of partition_sum to obtain a + 2b + 2c + d and applies the omega tactic to confirm the arithmetic identity with the total sum plus the middle pair.
why it matters
This identity supplies the algebraic step for middle_pair_sum_forced, which concludes that the middle pair equals 17 = W. It thereby supports the SDGT Forcing Theorem that selects the unique ordering (13, 11, 6, 8) for up quarks, leptons and down quarks under charge asymmetry. The result closes the partition-constraint portion of the forcing chain while leaving the origin of the specific step values open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.