module module high

`IndisputableMonolith.Masses.SDGTForcing`

The SDGTForcing module supplies algebraic identities for partition sums over three overlapping consecutive pairs together with ordering lemmas on spans A and B. Researchers deriving mass spectra from sector-dependent torsion cite these results to enforce the cell counts 11 and 6. The arguments proceed by direct expansion of the sum definitions and exhaustive case analysis on the middle pair.

claimFor four terms $a,b,c,d$ the partition sum over three overlapping consecutive pairs equals $a + 2b + 2c + d$.

background

The module imports AlphaDerivation, whose main result is the constructive derivation of $α^{-1}$ from cubic-ledger geometry including the Gauss-Bonnet extraction of $4π$ via vertex deficits, and SectorDependentTorsion, which proves that the set {13,11,6,8} comprises the Q₃ cell counts and satisfies the cyclic chain together with the partition $2^{D^D}+1=55$. The local setting is the masses domain, where these upstream facts are used to force sum and ordering constraints on consecutive pairs.

proof idea

The module is organized as a sequence of lemmas. step_sum and partition_sum_decomp supply the basic additive identities; middle_pair_sum_forced and only_11_6_sum_to_17 isolate the 11+6 case; ordering_A_spans, ordering_B_spans, ordering_A_unequal, ordering_B_equal and ordering_A_distinct_ends establish the required distinctness and equality properties. Each lemma is obtained by algebraic expansion followed by enumeration of the admissible integer assignments.

why it matters in Recognition Science

These identities close the algebraic side of the SDGT model and thereby support the mass-ladder constructions that rest on the T5 J-uniqueness, T7 eight-tick octave and T8 D=3 steps of the unified forcing chain. The results also tighten the alpha-band constraints already obtained in AlphaDerivation by confirming the shared-step arithmetic required by SectorDependentTorsion.

scope and limits

Does not derive explicit numerical mass values.
Does not treat non-consecutive or non-overlapping pairs.
Does not incorporate the gravitational constant G.
Does not address higher-dimensional generalizations beyond D=3.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants.AlphaDerivation module_import
IndisputableMonolith.Masses.SectorDependentTorsion module_import

declarations in this module (22)

def step_sum L48
theorem step_sum_eq L50
def partition_sum L54
theorem partition_sum_decomp L57
theorem middle_pair_sum_forced L63
theorem only_11_6_sum_to_17 L76
theorem middle_pair_is_11_6 L83
def ordering_A_spans L98
def ordering_B_spans L99
theorem ordering_A_unequal L101
theorem ordering_B_equal L102
theorem ordering_A_distinct_ends L105
theorem ordering_B_equal_ends L109
def Q_tilde_up L121
def Q_tilde_down L122
theorem charges_distinct L124
theorem larger_charge_larger_span L128
theorem sdgt_assignment_forced L138
theorem span_up_eq_2E L155
theorem span_lepton_eq_W L156
theorem span_down_eq_VF L159
theorem spans_partition_N3 L160