Proof: checkerboard monochromatic no-three-in-line bound for all n ≥ 6

Checkerboard.lean

@@ -0,0 +1 @@
+import Checkerboard.AllNTheorem

Checkerboard/AllNTheorem.lean

@@ -0,0 +1,25 @@
+import Checkerboard.AllNUpper
+import Checkerboard.N6Explicit
+
+/-!
+# Complete all-n checkerboard upper bound
+-/
+
+namespace Checkerboard
+
+/-- For every `n ≥ 6`, every no-three-in-line subset of either checkerboard
+color class has at most `2n-4` points. -/
+theorem checkerboard_upper_all_n {n parity : ℕ}
+    (hn : 6 ≤ n) (hp : parity = 0 ∨ parity = 1)
+    (s : Finset (Point n))
+    (hcolor : Monochromatic parity s) (hntil : NoThreeInLine s) :
+    s.card ≤ 2 * n - 4 := by
+  by_cases h6 : n = 6
+  · subst n
+    rcases hp with rfl | rfl
+    · exact n6_zero_upper s hcolor hntil
+    · exact n6_one_upper s hcolor hntil
+  · exact checkerboard_upper_from_seven (n := n) (parity := parity)
+      (s := s) (by omega) hp hcolor hntil
+
+end Checkerboard

Checkerboard/AllNUpper.lean

@@ -0,0 +1,196 @@
+import Checkerboard.QuadraticCosts
+
+/-!
+# The general checkerboard upper bound above the final 6×6 base case
+
+The quadratic line cover proves `|S| ≤ 2n-4` for both checkerboard colors on
+every board `n≥7`.  The thin color of the 7-board uses a separate exact small
+cover; all larger cases use the uniform quadratic family.
+-/
+
+namespace Checkerboard
+
+/-- Fat color on every odd board `2m+1`, `m≥3`. -/
+theorem odd_zero_upper {m : ℕ} (hm : 3 ≤ m)
+    (s : Finset (Point (2 * m + 1)))
+    (hcolor : Monochromatic 0 s) (hntil : NoThreeInLine s) :
+    s.card ≤ 4 * m - 2 := by
+  obtain ⟨hr, hc, hs, hd⟩ := oddQuadratic_nonnegative m 0
+  apply card_le_of_fourCertificate (oddQuadraticWeights m 0)
+      (q := 16 * (m : ℚ) ^ 2) (k := 4 * m - 2)
+  · positivity
+  · rw [oddQuadratic_cost_zero]
+    have hmQ : (3 : ℚ) ≤ m := by exact_mod_cast hm
+    have hmpos : (0 : ℚ) < m := by nlinarith
+    have hpoly : 0 < 2 * (m : ℚ) ^ 2 - 6 * m + 1 := by nlinarith
+    have hprod := mul_pos hmpos hpoly
+    have hk : 2 ≤ 4 * m := by omega
+    have hcast : (((4 * m - 2 : ℕ) : ℚ)) = 4 * (m : ℚ) - 2 := by
+      rw [Nat.cast_sub hk]
+      norm_num
+    rw [hcast]
+    nlinarith
+  · exact hr
+  · exact hc
+  · exact hs
+  · exact hd
+  · intro p
+    rw [oddQuadratic_coverage m 0 (Or.inl rfl) p.1 (hcolor p)]
+  · exact hntil
+
+/-- Thin color on every odd board `2m+1`, `m≥4`. -/
+theorem odd_one_upper {m : ℕ} (hm : 4 ≤ m)
+    (s : Finset (Point (2 * m + 1)))
+    (hcolor : Monochromatic 1 s) (hntil : NoThreeInLine s) :
+    s.card ≤ 4 * m - 2 := by
+  obtain ⟨hr, hc, hs, hd⟩ := oddQuadratic_nonnegative m 1
+  apply card_le_of_fourCertificate (oddQuadraticWeights m 1)
+      (q := 16 * (m : ℚ) ^ 2) (k := 4 * m - 2)
+  · positivity
+  · rw [oddQuadratic_cost_one]
+    have hmQ : (4 : ℚ) ≤ m := by exact_mod_cast hm
+    have hmpos : (0 : ℚ) < m := by nlinarith
+    have hpoly : 0 < 2 * (m : ℚ) ^ 2 - 6 * m - 2 := by nlinarith
+    have hprod := mul_pos hmpos hpoly
+    have hk : 2 ≤ 4 * m := by omega
+    have hcast : (((4 * m - 2 : ℕ) : ℚ)) = 4 * (m : ℚ) - 2 := by
+      rw [Nat.cast_sub hk]
+      norm_num
+    rw [hcast]
+    nlinarith
+  · exact hr
+  · exact hc
+  · exact hs
+  · exact hd
+  · intro p
+    rw [oddQuadratic_coverage m 1 (Or.inr rfl) p.1 (hcolor p)]
+  · exact hntil
+
+/-- Both colors on every even board `2m`, `m≥4`. -/
+theorem even_upper {m parity : ℕ} (hm : 4 ≤ m)
+    (hp : parity = 0 ∨ parity = 1)
+    (s : Finset (Point (2 * m)))
+    (hcolor : Monochromatic parity s) (hntil : NoThreeInLine s) :
+    s.card ≤ 4 * m - 4 := by
+  have hm1 : 1 ≤ m := by omega
+  have hmQ : (4 : ℚ) ≤ m := by exact_mod_cast hm
+  have hcenter : (0 : ℚ) < 2 * m - 1 := by nlinarith
+  have hpoly : 0 < 2 * (m : ℚ) ^ 2 - 8 * m + 3 := by nlinarith
+  have hprod := mul_pos hcenter hpoly
+  have hk : 4 ≤ 4 * m := by omega
+  have hcast : (((4 * m - 4 : ℕ) : ℚ)) = 4 * (m : ℚ) - 4 := by
+    rw [Nat.cast_sub hk]
+    norm_num
+  have hpCost := hp
+  obtain ⟨hr, hc, hs, hd⟩ := evenQuadratic_nonnegative m parity hm1
+  apply card_le_of_fourCertificate (evenQuadraticWeights m parity)
+      (q := 4 * ((2 * m : ℚ) - 1) ^ 2) (k := 4 * m - 4)
+  · positivity
+  · rcases hpCost with rfl | rfl
+    · rw [evenQuadratic_cost_zero m hm1, hcast]
+      nlinarith
+    · rw [evenQuadratic_cost_one m hm1, hcast]
+      nlinarith
+  · exact hr
+  · exact hc
+  · exact hs
+  · exact hd
+  · intro p
+    rw [evenQuadratic_coverage m parity hp hm1 p.1 (hcolor p)]
+  · exact hntil
+
+/-- Small exact cover for the exceptional thin color of the 7-board. -/
+def n7ThinWeights : FourWeights 7 where
+  row i := if i.1 = 0 ∨ i.1 = 6 then 1 else 0
+  column i := if i.1 = 0 ∨ i.1 = 6 then 1 else 0
+  sum j :=
+    if j.1 % 2 = 1 then
+      if Nat.dist j.1 6 = 1 then 2 else if Nat.dist j.1 6 = 3 then 1 else 0
+    else 0
+  difference j :=
+    if j.1 % 2 = 1 then
+      if Nat.dist j.1 6 = 1 then 2 else if Nat.dist j.1 6 = 3 then 1 else 0
+    else 0
+
+private theorem n7Thin_cost : fourCost n7ThinWeights = 32 := by
+  norm_num [fourCost, n7ThinWeights, Fin.sum_univ_succ, Nat.dist]
+  have hboundary :
+      ({x : Fin 7 | x = 0 ∨ (x : ℕ) = 6} : Finset (Fin 7)).card = 2 := by
+    decide
+  rw [hboundary]
+  norm_num
+
+private theorem n7Thin_nonnegative :
+    (∀ i, 0 ≤ n7ThinWeights.row i) ∧
+    (∀ i, 0 ≤ n7ThinWeights.column i) ∧
+    (∀ i, 0 ≤ n7ThinWeights.sum i) ∧
+    ∀ i, 0 ≤ n7ThinWeights.difference i := by
+  constructor
+  · intro i
+    fin_cases i <;> norm_num [n7ThinWeights]
+  constructor
+  · intro i
+    fin_cases i <;> norm_num [n7ThinWeights]
+  constructor
+  · intro i
+    fin_cases i <;> norm_num [n7ThinWeights, Nat.dist]
+  · intro i
+    fin_cases i <;> norm_num [n7ThinWeights, Nat.dist]
+
+private theorem n7Thin_cover :
+    ∀ p : Point 7, InColor 1 p → 3 ≤ fourCoverage n7ThinWeights p := by
+  rintro ⟨i, j⟩ hp
+  fin_cases i <;> fin_cases j
+  all_goals
+    norm_num [InColor] at hp
+  all_goals
+    norm_num [fourCoverage, n7ThinWeights, sumIndex,
+      differenceIndex, Nat.dist]
+
+/-- Exceptional thin-color bound on the 7-board. -/
+theorem n7_one_upper (s : Finset (Point 7))
+    (hcolor : Monochromatic 1 s) (hntil : NoThreeInLine s) : s.card ≤ 10 := by
+  obtain ⟨hr, hc, hs, hd⟩ := n7Thin_nonnegative
+  apply card_le_of_fourCertificate n7ThinWeights (q := 3) (k := 10)
+  · norm_num
+  · rw [n7Thin_cost]
+    norm_num
+  · exact hr
+  · exact hc
+  · exact hs
+  · exact hd
+  · intro p
+    exact n7Thin_cover p.1 (hcolor p)
+  · exact hntil
+
+/-- Fat-color bound on the 7-board. -/
+theorem n7_zero_upper (s : Finset (Point 7))
+    (hcolor : Monochromatic 0 s) (hntil : NoThreeInLine s) : s.card ≤ 10 := by
+  simpa using odd_zero_upper (m := 3) (by decide) s hcolor hntil
+
+/-- The general bound for all boards `n≥7` and either color. -/
+theorem checkerboard_upper_from_seven {n parity : ℕ}
+    (hn : 7 ≤ n) (hp : parity = 0 ∨ parity = 1)
+    (s : Finset (Point n))
+    (hcolor : Monochromatic parity s) (hntil : NoThreeInLine s) :
+    s.card ≤ 2 * n - 4 := by
+  obtain ⟨m, hEven | hOdd⟩ := n.even_or_odd'
+  · subst n
+    have hm : 4 ≤ m := by omega
+    have h := even_upper hm hp s hcolor hntil
+    omega
+  · subst n
+    have hm : 3 ≤ m := by omega
+    by_cases hsmall : m = 3
+    · subst m
+      rcases hp with rfl | rfl
+      · exact n7_zero_upper s hcolor hntil
+      · exact n7_one_upper s hcolor hntil
+    · have hm4 : 4 ≤ m := by omega
+      rcases hp with rfl | rfl
+      · have h := odd_zero_upper hm s hcolor hntil
+        omega
+      · have h := odd_one_upper hm4 s hcolor hntil
+        omega
+
+end Checkerboard

Checkerboard/FiberSums.lean

@@ -0,0 +1,120 @@
+import Mathlib
+
+namespace Checkerboard
+
+open scoped BigOperators
+
+section
+
+variable {α β R : Type*} [DecidableEq α] [DecidableEq β]
+
+def fiberCard (s : Finset α) (f : α → β) (b : β) : ℕ :=
+  (s.filter fun a => f a = b).card
+
+@[simp] theorem fiberCard_empty (f : α → β) (b : β) :
+    fiberCard ∅ f b = 0 := by simp [fiberCard]
+
+private theorem fiberCard_mul_eq_sum [CommSemiring R]
+    (s : Finset α) (f : α → β) (b : β) (g : β → R) :
+    (fiberCard s f b : R) * g b =
+      ∑ a ∈ s, if f a = b then g b else 0 := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp [fiberCard]
+  | @insert a s ha ih =>
+      by_cases h : f a = b
+      · have hnot : a ∉ s.filter fun x => f x = b := by
+          intro hmem
+          exact ha (Finset.mem_filter.mp hmem).1
+        have hfilter : (insert a s).filter (fun x => f x = b) =
+            insert a (s.filter fun x => f x = b) := by
+          ext x
+          by_cases hxa : x = a
+          · subst x; simp [ha, h]
+          · simp [hxa]
+        have ih' :
+            ((s.filter fun x => f x = b).card : R) * g b =
+              ∑ x ∈ s, if f x = b then g b else 0 := by
+          simpa [fiberCard] using ih
+        rw [fiberCard, hfilter]
+        rw [Finset.sum_insert ha, if_pos h]
+        simp only [Finset.card_insert_of_notMem hnot, Nat.cast_add, Nat.cast_one,
+          add_mul, one_mul]
+        rw [ih']
+        ac_rfl
+      · have hfilter : (insert a s).filter (fun x => f x = b) =
+            s.filter fun x => f x = b := by
+          ext x
+          by_cases hxa : x = a
+          · subst x; simp [ha, h]
+          · simp [hxa]
+        rw [fiberCard, hfilter]
+        rw [Finset.sum_insert ha, if_neg h]
+        simpa [fiberCard] using ih
+
+theorem sum_fiberCard_mul [Fintype β] [CommSemiring R]
+    (s : Finset α) (f : α → β) (g : β → R) :
+    ∑ b : β, (fiberCard s f b : R) * g b =
+      ∑ a ∈ s, g (f a) := by
+  classical
+  calc
+    ∑ b : β, (fiberCard s f b : R) * g b =
+        ∑ b : β, ∑ a ∈ s, if f a = b then g b else 0 := by
+          apply Finset.sum_congr rfl
+          intro b _
+          exact fiberCard_mul_eq_sum s f b g
+    _ = ∑ a ∈ s, ∑ b : β, if f a = b then g b else 0 := by
+          rw [Finset.sum_comm]
+    _ = ∑ a ∈ s, g (f a) := by
+          apply Finset.sum_congr rfl
+          intro a _
+          simp
+
+theorem sum_fiberCard [Fintype β] (s : Finset α) (f : α → β) :
+    ∑ b : β, fiberCard s f b = s.card := by
+  simpa using sum_fiberCard_mul (R := ℕ) s f (fun _ => 1)
+
+theorem sum_fiberCard_cast [Fintype β] [CommSemiring R]
+    (s : Finset α) (f : α → β) :
+    ∑ b : β, (fiberCard s f b : R) = (s.card : R) := by
+  simpa using sum_fiberCard_mul (R := R) s f (fun _ => 1)
+
+theorem card_le_sum_capacity [Fintype β]
+    (s : Finset α) (f : α → β) (capacity : β → ℕ)
+    (hcapacity : ∀ b, fiberCard s f b ≤ capacity b) :
+    s.card ≤ ∑ b, capacity b := by
+  rw [← sum_fiberCard s f]
+  exact Finset.sum_le_sum fun b _ => hcapacity b
+
+theorem sum_defect_mul [Fintype β]
+    (s : Finset α) (f : α → β) (capacity : β → ℕ)
+    (coordinate : β → ℝ)
+    (hcapacity : ∀ b, fiberCard s f b ≤ capacity b) :
+    (∑ b, ((capacity b - fiberCard s f b : ℕ) : ℝ) * coordinate b) =
+      (∑ b, (capacity b : ℝ) * coordinate b) -
+        ∑ a ∈ s, coordinate (f a) := by
+  calc
+    (∑ b, ((capacity b - fiberCard s f b : ℕ) : ℝ) * coordinate b) =
+        ∑ b, ((capacity b : ℝ) - (fiberCard s f b : ℝ)) * coordinate b := by
+          apply Finset.sum_congr rfl
+          intro b _
+          rw [Nat.cast_sub (hcapacity b)]
+    _ = (∑ b, (capacity b : ℝ) * coordinate b) -
+          ∑ b, (fiberCard s f b : ℝ) * coordinate b := by
+          simp only [sub_mul, Finset.sum_sub_distrib]
+    _ = (∑ b, (capacity b : ℝ) * coordinate b) -
+          ∑ a ∈ s, coordinate (f a) := by
+          rw [sum_fiberCard_mul]
+
+theorem sum_defect_mul_sq [Fintype β]
+    (s : Finset α) (f : α → β) (capacity : β → ℕ)
+    (coordinate : β → ℝ)
+    (hcapacity : ∀ b, fiberCard s f b ≤ capacity b) :
+    (∑ b, ((capacity b - fiberCard s f b : ℕ) : ℝ) * coordinate b ^ 2) =
+      (∑ b, (capacity b : ℝ) * coordinate b ^ 2) -
+        ∑ a ∈ s, coordinate (f a) ^ 2 := by
+  simpa using sum_defect_mul s f capacity (fun b => coordinate b ^ 2) hcapacity
+
+end
+
+end Checkerboard