ordering_B_spans
plain-language theorem explainer
The B-ordering spans definition supplies the triple of consecutive-pair sums (19, 17, 19) built from the generation steps 8, 11, 6, 13. Researchers on mass spectra or generation structure cite it when verifying that charge asymmetry selects orderings with equal end spans. It is introduced by direct arithmetic evaluation of the three overlapping sums with no lemmas required.
Claim. The B-ordering spans are the triple $(8 + 11, 11 + 6, 6 + 13)$.
background
The SDGT Forcing module proves that sector-dependent generation torsion is forced by three constraints: the partition constraint requiring three overlapping consecutive-pair spans to sum to N_3 = 2D^D + 1 = 55, lepton uniqueness that only the pair summing to 17 occupies the middle position, and charge asymmetry |Q̃_up| ≠ |Q̃_down|. The four step values are given as {V+F-C, E_pass, F, V} = {13, 11, 6, 8} and verified as Q_3 cell counts, though their origin from a single principle remains open per the module documentation.
proof idea
This is a direct definition that evaluates the three pair sums for the B ordering of the steps. No upstream lemmas are applied; the components are obtained by explicit addition of the listed integers.
why it matters
This definition is referenced by the theorem ordering_B_equal_ends, which establishes equal up and down spans for the B ordering as part of showing charge asymmetry forces the unique A ordering. It fills step 4 of the SDGT Forcing Theorem described in the module documentation. In the Recognition Science framework it supports the forcing chain that selects the mass ladder steps consistent with D = 3 and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.