module module high

`IndisputableMonolith.Masses.SDGTForcing`

This module defines partition and step sums for the SDGT cell counts {13,11,6,8} in the cubic ledger and verifies their algebraic relations under overlapping pairs and orderings. Researchers deriving mass spectra from Recognition Science geometry would cite these identities to confirm the 11+6=17 middle-pair constraint and the 55 partition. The argument consists of direct definitions followed by equality lemmas and exhaustive case analysis on the two admissible orderings of the cell counts.

claimFor consecutive cell counts $a,b,c,d$ the three overlapping pair sums equal the partition sum $a + 2b + 2c + d$.

background

The module sits inside the Recognition Science derivation of masses from the cubic ledger Q3. It imports AlphaDerivation, which obtains 4π from Gauss-Bonnet vertex deficits, and SectorDependentTorsion, whose doc-comment states that the integers {13,11,6,8} are the Q3 cell counts satisfying a cyclic chain and the partition 2^{D^D+1}=55 with shared steps between adjacent sectors. Local definitions include step_sum for incremental sector additions and partition_sum for the weighted sum over three consecutive overlapping pairs.

proof idea

This is a definition module with supporting lemmas. It introduces step_sum and partition_sum, proves their equality, decomposes the partition sum, forces the middle-pair sum, and then performs case analysis on orderings A and B to establish spans, equality of ends, and distinctness of the boundary values.

why it matters in Recognition Science

The module supplies the sum identities that close the algebraic constraints on the SDGT cell counts, thereby enabling the mass formula yardstick * phi^(rung-8+gap(Z)) on the phi-ladder. It feeds the eight-tick octave (T7) and D=3 (T8) structure by confirming the 11+6=17 relation and the 55 partition required for the Recognition framework.

scope and limits

Does not prove the cell counts equal {13,11,6,8}; those are established in SectorDependentTorsion.
Does not compute numerical mass values; only algebraic sum identities are shown.
Does not treat geometries beyond the cubic Q3 ledger.
Does not derive the fine-structure constant; relies on the imported AlphaDerivation module.

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