ordering_A_spans
plain-language theorem explainer
The definition computes the three consecutive-pair sums for the A ordering of generation steps {13, 11, 6, 8}, producing the triple (24, 17, 14). Researchers modeling sector-dependent generation torsion cite it when showing that charge asymmetry requires unequal end spans. It is implemented as a direct arithmetic evaluation of the sums 13+11, 11+6, and 6+8.
Claim. For the ordering (13, 11, 6, 8) of the step values, the spans are the consecutive sums $13+11$, $11+6$, $6+8$, yielding the triple $(24, 17, 14)$.
background
The SDGT Forcing module proves that sector-dependent generation torsion is forced by three constraints: the partition constraint (overlapping pair sums total N₃ = 55), lepton uniqueness (only {11, 6} sums to 17), and charge asymmetry (|Q̃_up| ≠ |Q̃_down|). The four step values {13, 11, 6, 8} are assigned as up quarks {13, 11}, leptons {11, 6}, down quarks {6, 8}. This definition supplies the spans for the A ordering (13, 11, 6, 8). The upstream theorem middle_pair_is_11_6 establishes that any middle pair summing to 17 and drawn from the set must be {11, 6} in either order.
proof idea
This is a one-line definition that directly evaluates the three consecutive sums 13+11, 11+6, and 6+8 to produce the tuple (24, 17, 14).
why it matters
It is referenced by the theorem ordering_A_distinct_ends, which proves the A ordering has distinct up and down spans. This completes the forcing step in the SDGT Forcing Theorem that selects the unique ordering (13, 11, 6, 8) under charge asymmetry. The module notes that the origin of the specific step values {13, 11, 6, 8} as Q₃ cell counts remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.