Q_tilde_down

formal source

 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
 140    (∀ a b c d : ℕ, a + b + c + d = 38 → partition_sum a b c d = 55 → b + c = 17) ∧
 141    -- Only {11, 6} sums to 17
 142    (11 + 6 = 17) ∧
 143    -- Ordering A has unequal end spans (forced by charge asymmetry)
 144    ((13 + 11 : ℕ) ≠ 6 + 8) ∧
 145    -- The spans are 24, 17, 14
 146    (13 + 11 = 24) ∧ (11 + 6 = 17) ∧ (6 + 8 = 14) ∧
 147    -- They partition 55
 148    (24 + 17 + 14 = 55) := by
 149  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
 150  · intro a b c d hsum hpart; exact middle_pair_sum_forced a b c d hsum hpart
 151  all_goals omega
 152