ordering_B_equal_ends
plain-language theorem explainer
Ordering B in the sector-dependent generation torsion has equal endpoint spans. Researchers modeling forced mass hierarchies under Recognition Science constraints cite it when excluding charge-symmetric configurations. The proof is a one-line computational check via the native_decide tactic on the precomputed span tuple.
Claim. For the span tuple $s$ of ordering B, the first component equals the second component of the second pair: $s_1 = s_{2,2}$.
background
The SDGT Forcing module proves sector-dependent generation torsion is forced by three constraints: the partition sum of three overlapping consecutive-pair spans equals N₃ = 55, lepton uniqueness selects only the middle pair {11, 6}, and charge asymmetry |Q̃_up| = 4 ≠ 2 = |Q̃_down| requires unequal end spans. From the module documentation: 'the assignment Up quarks: {13, 11}, Leptons: {11, 6}, Down quarks: {6, 8} is the UNIQUE assignment consistent with charge asymmetry.' This theorem verifies the equal-ends property of the alternative ordering B.
proof idea
It is a one-line wrapper that applies the native_decide tactic directly to the equality ordering_B_spans.1 = ordering_B_spans.2.2, confirming by computation that the B configuration has equal endpoint spans.
why it matters
The result supports exclusion of ordering B inside the SDGT Forcing Theorem, which selects the unique (13, 11, 6, 8) assignment under charge asymmetry. It fills the charge-asymmetry step of the module while leaving open the single-principle derivation of the step values themselves. The construction sits inside the Recognition Science mass ladder and phi-ladder framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.