module module high

`IndisputableMonolith.Masses.SectorDependentTorsion`

SectorDependentTorsion supplies the geometric primitives for the cubic polytope Q_D at D=3, including its vertices as 0-cells, edges, faces, and the sector quantities S0, S1, S2. Mass-spectrum researchers cite these objects when enumerating generation steps or proving torsion-forcing constraints. The module consists entirely of definitions with no theorems or proofs.

claimThe vertices of the cubic polytope $Q_D$ (its 0-cells), together with the edges, faces, and sector-dependent quantities $S_0$, $S_1$, $S_2$ evaluated at $D=3$.

background

The module sits inside the Recognition Science treatment of masses and inherits the cubic-ledger geometry from the Alpha Derivation module, whose doc-comment states that it supplies a constructive derivation of the fine-structure constant from vertex deficits of Q_3 via Gauss-Bonnet. It introduces the 0-cells (vertices) of Q_D, the associated 1-cells and 2-cells, and the three sector invariants S0, S1, S2 that encode torsion dependence across generations. These objects are the concrete carriers of the Euler characteristic and cube-invariance statements used downstream.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions feed the SDGT Forcing theorem, whose doc-comment states that sector-dependent generation torsion is forced by the partition constraint summing to N_3=55 and the lepton-uniqueness condition, and the Step Value Enumeration module, whose doc-comment identifies the step values {13,11,6,8} as Q_3 cube invariants via the Euler characteristic V-E+F=2 on the boundary sphere. The module therefore supplies the geometric substrate for the mass-sector forcing chain.

scope and limits

Does not contain theorems or proofs.
Does not compute numerical values of constants.
Does not treat dimensions other than D=3.
Does not derive the mass ladder or phi-ladder relations.

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Masses.SDGTForcing module_import
IndisputableMonolith.Masses.StepValueEnumeration module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants.AlphaDerivation module_import

declarations in this module (73)

def cube_vertices' L39
def cube_edges' L42
def cube_faces' L45
def cube_body L48
theorem vertices_at_D3 L50
theorem edges_at_D3 L51
theorem faces_at_D3 L52
def S0 L57
def S1 L60
def S2 L63
theorem S0_at_D3 L65
theorem S1_at_D3 L66
theorem S2_at_D3 L67
def N0 L75
def N1 L78
def N2 L81
theorem N0_at_D3 L83
theorem N1_at_D3 L84
theorem N2_at_D3 L85
theorem N0_eq_W_at_D3 L92
theorem N0_ne_W_at_D1 L95
theorem N0_ne_W_at_D2 L98
theorem N0_ne_W_at_D4 L101
theorem N0_ne_W_at_D5 L104
theorem N2_minus_N1 L114
theorem N1_minus_N0 L115
theorem N_diff_eq_edges_at_D3 L118
def lepton_step_12 L131
def lepton_step_23 L132
theorem lepton_step_12_eq L134
theorem lepton_step_23_eq L135
theorem lepton_total_span L137
def down_step_12 L150
def down_step_23 L151
theorem down_step_12_eq L153
theorem down_step_23_eq L154
theorem down_total_span L156
theorem down_span_eq_W_minus_D L159
def down_rung_gen1 L163
def down_rung_gen2 L164
def down_rung_gen3 L165
theorem down_rung_gen1_eq L167
theorem down_rung_gen2_eq L168
theorem down_rung_gen3_eq L169
theorem down_generation_ordering L172
def vertex_face_excess L197
theorem vertex_face_excess_at_D3 L199
def up_step_12 L202
def up_step_23 L203
theorem up_step_12_eq L205
theorem up_step_23_eq L206
theorem up_total_span L209
def up_rung_gen1 L213
def up_rung_gen2 L214
def up_rung_gen3 L215
theorem up_rung_gen1_eq L217
theorem up_rung_gen2_eq L218
theorem up_rung_gen3_eq L219
theorem up_generation_ordering L222
def cross_sector_shift_down L232
theorem cross_sector_shift_eq L234
theorem lepton_span_eq_N0 L241
theorem down_span_plus_D_eq_W L245
theorem up_span_eq_twice_edges L249
def N3' L253
theorem N3'_at_D3 L254
theorem sector_spans_partition_N3 L257
theorem cyclic_chain L263
theorem up_lepton_share_Epass L270
theorem lepton_down_share_F L271
theorem up_minus_lepton_span L274
theorem lepton_minus_down_span L278
theorem total_cells_eq_D_pow_D L283