module module moderate

`IndisputableMonolith.Masses.SectorDependentTorsion`

SectorDependentTorsion supplies the D=3 cube invariants (vertices, edges, faces, body) and the three sector torsion parameters S0, S1, S2 for the Recognition mass ladder. Researchers working on SDGT forcing or step-value enumeration cite these definitions. The module is purely definitional; it contains no theorems or proofs.

claimThe 0-cells (vertices) of the cubic polytope $Q_D$, together with the derived edge, face and body counts at $D=3$, and the sector-dependent torsion values $S_0,S_1,S_2$ satisfying the Euler relation $V-E+F=2$ on the boundary sphere.

background

The module imports AlphaDerivation, whose doc-comment states it supplies a constructive derivation of $\alpha^{-1}$ from the geometry of the cubic ledger, including the structural derivation of $4\pi$ via vertex deficits of $Q_3$. It introduces the sibling definitions cube_vertices', cube_edges', cube_faces', cube_body, vertices_at_D3, edges_at_D3, faces_at_D3 together with S0, S1, S2 and their D=3 specializations. These objects encode the discrete geometry underlying the Recognition Science mass formula and the eight-tick octave at D=3.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The definitions feed the SDGTForcing theorem, which proves sector-dependent generation torsion is forced by the partition constraint summing to $N_3=55$ and the lepton-uniqueness condition on {11,6}. They also supply the cube invariants required by StepValueEnumeration to identify the generation-step values {13,11,6,8} via the Euler characteristic at $\partial Q_3 \cong S^2$.

scope and limits

Does not contain any theorem or proof.
Does not compute numerical mass values.
Does not state the full SDGT forcing argument.
Does not address higher-dimensional cases beyond D=3.

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