larger_charge_larger_span
plain-language theorem explainer
The declaration shows that the up-sector integerized charge exceeds the down-sector value, forcing a larger span in the SDGT partition of N3=55. Researchers modeling generation torsion via charge asymmetry would cite this to lock in the ordering with up quarks on the larger end. The proof reduces directly to the constant definitions of the charges and applies arithmetic comparison.
Claim. $|Q̃_{up}| > |Q̃_{down}| ∧ (13 + 11) > (6 + 8)$, where the integerized charges are defined by $|Q̃_{up}| = 4$ and $|Q̃_{down}| = 2$.
background
The SDGT Forcing module establishes that sector-dependent generation torsion is forced by three constraints: the partition sum of overlapping consecutive-pair spans equals N3 = 55, lepton uniqueness restricts the middle pair to {11,6}, and charge asymmetry distinguishes the ends. The referenced definitions set Q_tilde_up to 4 (from |6 × 2/3|) and Q_tilde_down to 2 (from |6 × 1/3|). Upstream results on cellular automata steps and backpropagation completeness supply the locality and consistency background for the partition arithmetic.
proof idea
The term proof unfolds the definitions of Q_tilde_up and Q_tilde_down to the constants 4 and 2. Constructor splits the conjunction into two goals, after which omega discharges the inequalities 4 > 2 and 24 > 14.
why it matters
This step completes the charge asymmetry argument inside the SDGT forcing theorem, showing that |Q̃_up| ≠ |Q̃_down| selects the unique ordering (13,11,6,8) over symmetric alternatives. It directly supports the module's main claim that the assignment up {13,11}, leptons {11,6}, down {6,8} is the only one consistent with the three constraints. The open question remains the first-principles derivation of the four step values themselves.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.