middle_pairs_are_11_6

formal source

  75def middle_pairs_summing_to_17 : List (ℕ × ℕ) :=
  76  [(6, 11), (11, 6)]
  77
  78theorem middle_pairs_are_11_6 :
  79    ∀ (b c : ℕ), b ∈ natural_invariants_D3 → c ∈ natural_invariants_D3 →
  80    b + c = 17 → b ≠ c →
  81    (b = 6 ∧ c = 11) ∨ (b = 11 ∧ c = 6) ∨
  82    -- Any other pair summing to 17 among our natural invariants
  83    (b = 17 ∧ c = 0) ∨ (b = 0 ∧ c = 17) := by
  84  intro b c hb hc hsum _hne
  85  simp [natural_invariants_D3, List.mem_cons] at hb hc
  86  omega
  87
  88/-- Excluding zero (since 0 is not a "natural cube invariant"), only
  89    {11, 6} appears in the middle pair position. -/
  90theorem middle_pair_unique_nonzero :
  91    ∀ (b c : ℕ), b ∈ natural_invariants_D3 → c ∈ natural_invariants_D3 →
  92    b + c = 17 → b ≠ c → b ≠ 0 → c ≠ 0 →
  93    (b = 6 ∧ c = 11) ∨ (b = 11 ∧ c = 6) := by
  94  intro b c hb hc hsum hne hb0 hc0
  95  have h := middle_pairs_are_11_6 b c hb hc hsum hne
  96  rcases h with h | h | h | h
  97  · exact Or.inl h
  98  · exact Or.inr h
  99  · exact absurd h.2 hc0
 100  · exact absurd h.1 hb0
 101
 102/-! ## Constraint 2: Endpoint pair (a, d) sums to 21
 103
 104From the partition constraint a + 2b + 2c + d = 55 with b+c = 17:
 105a + 34 + d = 55, so a + d = 21.
 106-/
 107
 108/-- All pairs (a, d) from natural invariants with a + d = 21,