ordering_B_equal_ends

formal source

 106    ordering_A_spans.1 ≠ ordering_A_spans.2.2 := by native_decide
 107
 108/-- Ordering B has equal up/down spans. -/
 109theorem ordering_B_equal_ends :
 110    ordering_B_spans.1 = ordering_B_spans.2.2 := by native_decide
 111
 112/-! ## Step 4: Charge Asymmetry Forces Ordering A
 113
 114The integerized charges are |Q̃_up| = 4 and |Q̃_down| = 2.
 115Since 4 ≠ 2, the up and down sectors are physically distinct.
 116Equal spans would imply charge-degenerate mass hierarchies.
 117
 118Ordering B (equal spans) is therefore excluded.
 119Ordering A (unequal spans) is forced. -/
 120
 121def Q_tilde_up : ℕ := 4      -- |6 × 2/3| = 4
 122def Q_tilde_down : ℕ := 2    -- |6 × 1/3| = 2
 123
 124theorem charges_distinct : Q_tilde_up ≠ Q_tilde_down := by native_decide
 125
 126/-- The larger charge gets the larger span.
 127    |Q̃_up| = 4 > |Q̃_down| = 2, so span_up = 24 > span_down = 14. -/
 128theorem larger_charge_larger_span :
 129    Q_tilde_up > Q_tilde_down ∧
 130    (13 + 11 : ℕ) > (6 + 8) := by
 131  unfold Q_tilde_up Q_tilde_down
 132  constructor <;> omega
 133
 134/-! ## Main Theorem: SDGT is Forced -/
 135
 136/-- The complete forcing result: given the four step values and the
 137    partition + charge constraints, the SDGT assignment is unique. -/
 138theorem sdgt_assignment_forced :
 139    -- The partition constraint forces middle pair to sum to W