middle_pair_unique_nonzero

formal source

  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,
 109    excluding {11, 6} (already used as middle) and ordered pairs. -/
 110def endpoint_pairs_summing_to_21 : List (ℕ × ℕ) :=
 111  [(7, 14), (8, 13), (14, 7), (13, 8)]
 112  -- Note: 1+20, 6+15, 11+10 excluded because they use middle values or
 113  -- values outside the natural set. 20 and 15 are possible but form less
 114  -- natural chains (see analysis below).
 115
 116/-- There exist multiple valid endpoint pairs from the natural invariants.
 117    This is the heart of the openness: uniqueness cannot be proved without
 118    additional structural constraints. -/
 119theorem endpoint_pairs_not_unique :
 120    ∃ (a₁ d₁ a₂ d₂ : ℕ),