sdgt_assignment_forced
plain-language theorem explainer
The theorem establishes that the sector-dependent generation torsion assignment is uniquely determined by the partition sum equaling 55 together with the charge asymmetry constraint. Physicists modeling mass hierarchies via Recognition Science would cite this result to confirm the forced ordering of generation steps. The proof applies the middle-pair lemma to the sum and partition hypotheses then resolves the remaining numerical identities and inequalities via omega.
Claim. Given natural numbers $a,b,c,d$ with $a+b+c+d=38$, if the sum of the three overlapping consecutive-pair spans equals 55 then the middle pair sums to 17. Moreover $11+6=17$, the end spans are unequal since $13+11≠6+8$, the spans evaluate to $13+11=24$, $11+6=17$, $6+8=14$, and these three values sum to 55.
background
The SDGT Forcing module shows that sector-dependent generation torsion is forced rather than merely compatible with three constraints: the partition constraint (sum of three overlapping consecutive-pair spans equals N₃=55), lepton uniqueness (only {11,6} sums to W=17), and charge asymmetry (|Q̃_up|≠|Q̃_down| forces unequal end spans). The upstream middle_pair_sum_forced lemma states: if the partition sum must equal 55 and the element sum is 38, the middle pair must sum to 17. The four step values {13,11,6,8} are taken as given from SectorDependentTorsion and correspond to the unique ordering up quarks {13,11}, leptons {11,6}, down quarks {6,8}.
proof idea
The proof is a term-mode refinement that splits the conjunction into seven subgoals. The first subgoal is discharged by applying the middle_pair_sum_forced lemma to the sum and partition hypotheses. The remaining six subgoals are pure numerical identities and inequalities, all closed by the omega tactic.
why it matters
This declaration completes the forcing argument for the unique SDGT assignment in the masses domain. It directly supports the claim in the module documentation that the ordering (13,11,6,8) is the unique assignment consistent with the partition constraint and charge asymmetry. The result touches the open question noted in the module doc that the four step values themselves are not yet derived from a single principle. In the broader framework it aligns with the eight-tick octave and D=3 underlying the partition sum 55.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.