partition_sum
plain-language theorem explainer
Partition sum defines the weighted total a + 2b + 2c + d for four natural numbers that represent consecutive generation steps under the SDGT partition constraint. Researchers modeling forced sector assignments in Recognition Science masses would cite this definition when decomposing the total span of 55 into element sum and middle pair. It is supplied as a direct arithmetic definition to support downstream omega reductions.
Claim. For natural numbers $a, b, c, d$, the partition sum is $p(a,b,c,d) := a + 2b + 2c + d$. This encodes the sum of three overlapping consecutive-pair spans that must total $N_3 = 55$.
background
In the SDGT Forcing module the partition constraint requires that the sum of three overlapping consecutive-pair spans equals $N_3 = 2D^D + 1 = 55$, where $D = 3$ spatial dimensions follows from the Recognition Science forcing chain. The four step values $a, b, c, d$ stand for the generation steps assigned to up quarks, leptons and down quarks. The definition captures the double-counting of the middle pair in the overlapping spans.
proof idea
This is a direct definition that unfolds immediately to the arithmetic expression $a + 2b + 2c + d$. Downstream theorems apply it by unfolding followed by omega, as in partition_sum_decomp which equates the partition sum to the element sum plus the middle pair sum.
why it matters
The definition supports the forcing theorems that establish the unique SDGT assignment. It feeds middle_pair_sum_forced, whose doc-comment states: 'If the partition sum must equal 55 and element sum is 38, the middle pair must sum to 17 = W.' It also feeds sdgt_assignment_forced, which concludes the complete forcing result under partition, lepton uniqueness and charge asymmetry constraints. The construction implements the first of the three constraints listed in the module documentation and connects to the framework landmark $D = 3$ via the value of $N_3$. The module documentation notes that the specific step values themselves remain open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.