ordering_A_unequal
plain-language theorem explainer
The inequality 13 + 11 ≠ 6 + 8 enforces the charge asymmetry that distinguishes end spans in the sector-dependent generation torsion construction. Researchers deriving forced mass orderings from Recognition Science would cite it to lock in the unique assignment of spans to up quarks, leptons, and down quarks. The proof reduces the claim to elementary arithmetic via a single decision-procedure call.
Claim. $13 + 11 ≠ 6 + 8$
background
The SDGT Forcing module proves that sector-dependent generation torsion is forced rather than merely compatible. Three constraints operate: the partition constraint that three overlapping consecutive-pair spans sum to N₃ = 55, lepton uniqueness that only the pair summing to 17 occupies the middle position, and charge asymmetry that the absolute values of the effective charges on up and down sectors differ. The four step values {13, 11, 6, 8} are already verified as Q₃ cell counts in SectorDependentTorsion; the present theorem supplies the final numerical check that selects the ordering.
proof idea
The proof is a one-line wrapper that invokes the omega tactic on the concrete arithmetic statement 13 + 11 ≠ 6 + 8.
why it matters
The result supplies the charge-asymmetry step inside the SDGT Forcing Theorem, which in turn fixes the unique span assignment (up quarks {13,11}, leptons {11,6}, down quarks {6,8}). It therefore anchors the rung placements on the phi-ladder used by the mass formula. The module documentation notes that the origin of the four step values themselves remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.