middle_pair_sum_forced

formal source

  60
  61/-- If the partition sum must equal 55 and element sum is 38,
  62    the middle pair must sum to 17 = W. -/
  63theorem middle_pair_sum_forced (a b c d : ℕ)
  64    (hsum : a + b + c + d = 38)
  65    (hpart : partition_sum a b c d = 55) :
  66    b + c = 17 := by
  67  have := partition_sum_decomp a b c d
  68  omega
  69
  70/-! ## Step 2: Uniqueness — Only {11, 6} sums to 17
  71
  72Among the four values {13, 11, 6, 8}, the only pair summing to 17
  73is {11, 6} = {E_pass, F}. -/
  74
  75/-- Exhaustive check: no other pair from {13, 11, 6, 8} sums to 17. -/
  76theorem only_11_6_sum_to_17 :
  77    (13 + 11 ≠ 17) ∧ (13 + 6 ≠ 17) ∧ (13 + 8 ≠ 17) ∧
  78    (11 + 8 ≠ 17) ∧ (6 + 8 ≠ 17) ∧
  79    (11 + 6 = 17) := by
  80  refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;> omega
  81
  82/-- The middle pair {b, c} must be {11, 6} (in either order). -/
  83theorem middle_pair_is_11_6 (b c : ℕ)
  84    (hbc : b + c = 17)
  85    (hb : b ∈ ({13, 11, 6, 8} : Finset ℕ))
  86    (hc : c ∈ ({13, 11, 6, 8} : Finset ℕ))
  87    (_hne : b ≠ c) :
  88    (b = 11 ∧ c = 6) ∨ (b = 6 ∧ c = 11) := by
  89  simp [Finset.mem_insert, Finset.mem_singleton] at hb hc
  90  omega
  91
  92/-! ## Step 3: The Two Orderings
  93