ordering_A_distinct_ends
plain-language theorem explainer
The declaration establishes that the first and third components of the span tuple for ordering A differ. Researchers modeling quark and lepton mass assignments under sector-dependent torsion would cite it to enforce charge asymmetry in the generation ladder. The proof is a one-line numerical verification via native decision procedure on the concrete values.
Claim. Let $S = (13 + 11, 11 + 6, 6 + 8)$. Then the first component of $S$ is unequal to the third component of $S$.
background
The SDGT Forcing module proves that sector-dependent generation torsion is forced by three constraints: the partition sum of overlapping consecutive-pair spans equals 55, only the pair summing to 17 can occupy the lepton sector, and charge asymmetry requires unequal end spans. The upstream definition ordering_A_spans computes these consecutive sums for the sequence 13, 11, 6, 8 as the tuple (24, 17, 14). The sibling result middle_pair_is_11_6 forces the middle pair to be 11 and 6 in either order, while the has class from AsteroidOreSpectroscopy supplies the spectral-peak rung characterization used to rank the underlying mass steps.
proof idea
The proof is a one-line wrapper that applies native_decide to the concrete inequality 24 ≠ 14.
why it matters
This result supplies the final numerical check for the charge-asymmetry clause in the SDGT Forcing Theorem, confirming that the assignment up quarks {13, 11}, leptons {11, 6}, down quarks {6, 8} is the unique partition of 55 consistent with |Q̃_up| ≠ |Q̃_down|. It closes the local forcing argument for the mass ladder while leaving open the derivation of the four step values themselves from the Recognition functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.