pith. machine review for the scientific record. sign in
theorem proved term proof

middle_pair_unique_nonzero

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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

proof body

Term-mode proof.

  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. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (6)

Lean names referenced from this declaration's body.