spans_partition_N3
plain-language theorem explainer
Researchers deriving the unique sector assignment in the SDGT forcing theorem cite the equality 24 + 17 + 14 = N3'(3) to verify that the three overlapping spans partition exactly to the required N3 value of 55. This numerical check closes one of the three forcing constraints listed in the module. The proof proceeds by a single native_decide evaluation of the left-hand arithmetic against the explicit formula for N3' at d=3.
Claim. $24 + 17 + 14 = N_3'(3)$ where $N_3'(d) = 2(V(d) + E(d) + F(d) + C) + 1$ and $V,E,F,C$ denote the cube vertices, edges, faces, and body counts at dimension $d$.
background
The SDGT Forcing module establishes that sector-dependent generation torsion is forced by three constraints, the first being the partition constraint requiring three overlapping consecutive-pair spans to sum to N3 = 55. N3' is defined upstream as N3'(d) := 2*(cube_vertices' d + cube_edges' d + cube_faces' d + cube_body) + 1, which equals 55 at d=3. The module states that given step values {13,11,6,8} the assignment up quarks {13,11}, leptons {11,6}, down quarks {6,8} is the unique one consistent with charge asymmetry.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the arithmetic equality directly against the definition of N3' at dimension 3.
why it matters
This theorem closes the partition constraint inside the SDGT Forcing Theorem, confirming that the spans sum to N3' 3 = 55 and thereby supporting the unique ordering (13,11,6,8). It relies on the N3' definition from SectorDependentTorsion and feeds the claim that the lepton sector must occupy the middle position. The module notes that the four step values themselves remain open, not yet derived from a single principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.