partition_sum_decomp
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the four step values {13, 11, 6, 8} from a single principle.
- Does not prove lepton uniqueness or charge asymmetry.
- Applies only to natural-number inputs and the given partition definition.
- Does not connect to J-uniqueness, phi-ladder mass formulas or alpha-band constraints.
Lean usage
have := partition_sum_decomp a b c dformal statement (Lean)
57theorem partition_sum_decomp (a b c d : ℕ) :
58 partition_sum a b c d = (a + b + c + d) + (b + c) := by
proof body
Term-mode proof.
59 unfold partition_sum; omega
60
61/-- If the partition sum must equal 55 and element sum is 38,
62 the middle pair must sum to 17 = W. -/