ordering_B_equal
plain-language theorem explainer
The arithmetic identity 8 + 11 = 6 + 13 is verified to confirm consistent span sums under the partition constraint in the SDGT forcing argument. Researchers deriving the unique mass-sector ordering (13, 11, 6, 8) for up quarks, leptons, and down quarks would cite this step to close the arithmetic check on overlapping consecutive-pair sums equaling N_3 = 55. The proof reduces directly to the omega decision procedure for natural-number equalities.
Claim. $8 + 11 = 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 forcing only {11, 6} to sum to W = 17, and charge asymmetry requiring unequal end spans. This yields the unique assignment with up quarks on {13, 11}, leptons on {11, 6}, and down quarks on {6, 8}. Upstream, the active edge count A per fundamental tick is defined as 1 in both IntegrationGap and Anchor, while the actualization operator A maps a configuration to the J-cost minimizer over its possibilities.
proof idea
The proof is a one-line wrapper that applies the omega tactic to discharge the natural-number equality.
why it matters
This equality supplies the arithmetic verification for ordering B inside the SDGT Forcing Theorem, which establishes that the four step values produce the unique sector assignment consistent with charge asymmetry. It supports the mass formula on the phi-ladder by confirming the span sums required for the forced ordering. The module documentation notes that the step values themselves remain open, verified only as Q_3 cell counts rather than derived from a single principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.