diff --git a/Checkerboard.lean b/Checkerboard.lean
new file mode 100644
index 00000000..57ed8d63
--- /dev/null
+++ b/Checkerboard.lean
@@ -0,0 +1 @@
+import Checkerboard.AllNTheorem
diff --git a/Checkerboard/AllNTheorem.lean b/Checkerboard/AllNTheorem.lean
new file mode 100644
index 00000000..02de75f4
--- /dev/null
+++ b/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
diff --git a/Checkerboard/AllNUpper.lean b/Checkerboard/AllNUpper.lean
new file mode 100644
index 00000000..712e277a
--- /dev/null
+++ b/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
diff --git a/Checkerboard/FiberSums.lean b/Checkerboard/FiberSums.lean
new file mode 100644
index 00000000..3ab7902d
--- /dev/null
+++ b/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
diff --git a/Checkerboard/FinPolynomialSums.lean b/Checkerboard/FinPolynomialSums.lean
new file mode 100644
index 00000000..a082ecb7
--- /dev/null
+++ b/Checkerboard/FinPolynomialSums.lean
@@ -0,0 +1,81 @@
+import Checkerboard.PolynomialSums
+
+/-!
+# Polynomial sums over `Fin`
+-/
+
+namespace Checkerboard
+
+open scoped BigOperators
+
+/-- Sum of an affine square over `Fin n`. -/
+theorem sum_fin_affine_sq (n : ℕ) (a b : ℚ) :
+    (∑ i : Fin n, (a * (i.1 : ℚ) + b) ^ 2) =
+      a ^ 2 * ((n : ℚ) * ((n : ℚ) - 1) * (2 * (n : ℚ) - 1) / 6) +
+      2 * a * b * ((n : ℚ) * ((n : ℚ) - 1) / 2) +
+      (n : ℚ) * b ^ 2 := by
+  rw [Finset.sum_fin_eq_sum_range]
+  convert sum_range_affine_sq n a b using 1
+  apply Finset.sum_congr rfl
+  intro i hi
+  rw [Finset.mem_range] at hi
+  rw [dif_pos hi]
+
+/-- Sum of the centered axis-square weights. -/
+theorem axis_quadratic_sum (n : ℕ) :
+    (∑ i : Fin n, (2 * (i.1 : ℚ) - ((n : ℚ) - 1)) ^ 2) =
+      (n : ℚ) * ((n : ℚ) ^ 2 - 1) / 3 := by
+  have h := sum_fin_affine_sq n (2 : ℚ) (1 - (n : ℚ))
+  calc
+    (∑ i : Fin n, (2 * (i.1 : ℚ) - ((n : ℚ) - 1)) ^ 2) =
+        ∑ i : Fin n, (2 * (i.1 : ℚ) + (1 - (n : ℚ))) ^ 2 := by
+          apply Finset.sum_congr rfl
+          intro i _
+          ring
+    _ = 2 ^ 2 * ((n : ℚ) * ((n : ℚ) - 1) * (2 * (n : ℚ) - 1) / 6) +
+        2 * 2 * (1 - (n : ℚ)) * ((n : ℚ) * ((n : ℚ) - 1) / 2) +
+        (n : ℚ) * (1 - (n : ℚ)) ^ 2 := h
+    _ = (n : ℚ) * ((n : ℚ) ^ 2 - 1) / 3 := by ring
+
+/-- Full sum of a quadratic diagonal cap over `Fin (2N+1)`. -/
+theorem fin_quadratic_cap_sum (N : ℕ) :
+    (∑ j : Fin (2 * N + 1),
+      2 * ((N : ℚ) ^ 2 - ((j.1 : ℚ) - N) ^ 2)) =
+      2 * (N : ℚ) * (2 * (N : ℚ) - 1) * (2 * (N : ℚ) + 1) / 3 := by
+  rw [Finset.sum_fin_eq_sum_range]
+  convert sum_range_quadratic_cap N using 1
+  apply Finset.sum_congr rfl
+  intro j hj
+  rw [Finset.mem_range] at hj
+  rw [dif_pos hj]
+
+/-- Even-indexed cap sum over `Fin (4m+1)`. -/
+theorem fin_even_quadratic_cap_sum (m : ℕ) :
+    (∑ j : Fin (4 * m + 1),
+      if j.1 % 2 = 0 then
+        2 * ((2 * m : ℚ) ^ 2 - ((j.1 : ℚ) - 2 * m) ^ 2)
+      else 0) =
+      8 * (m : ℚ) * (2 * (m : ℚ) - 1) *
+        (2 * (m : ℚ) + 1) / 3 := by
+  rw [Finset.sum_fin_eq_sum_range]
+  convert even_quadratic_cap_sum m using 1
+  apply Finset.sum_congr rfl
+  intro j hj
+  rw [Finset.mem_range] at hj
+  rw [dif_pos hj]
+
+/-- Odd-indexed cap sum over `Fin (4m+1)`. -/
+theorem fin_odd_quadratic_cap_sum (m : ℕ) :
+    (∑ j : Fin (4 * m + 1),
+      if j.1 % 2 = 1 then
+        2 * ((2 * m : ℚ) ^ 2 - ((j.1 : ℚ) - 2 * m) ^ 2)
+      else 0) =
+      4 * (m : ℚ) * (8 * (m : ℚ) ^ 2 + 1) / 3 := by
+  rw [Finset.sum_fin_eq_sum_range]
+  convert odd_quadratic_cap_sum m using 1
+  apply Finset.sum_congr rfl
+  intro j hj
+  rw [Finset.mem_range] at hj
+  rw [dif_pos hj]
+
+end Checkerboard
diff --git a/Checkerboard/FourCertificate.lean b/Checkerboard/FourCertificate.lean
new file mode 100644
index 00000000..d554d450
--- /dev/null
+++ b/Checkerboard/FourCertificate.lean
@@ -0,0 +1,198 @@
+import Checkerboard.Model
+import Checkerboard.FiberSums
+
+/-!
+# Four-direction rational line-cover certificates
+
+A no-three-in-line set has capacity at most two on every row, column, sum
+diagonal, and difference diagonal. This file packages that observation as a
+generic exact rational certificate theorem.
+-/
+
+namespace Checkerboard
+
+open scoped BigOperators
+
+def sumIndex {n : ℕ} (p : Point n) : Fin (2 * n - 1) :=
+  ⟨p.1.1 + p.2.1, by omega⟩
+
+def differenceIndex {n : ℕ} (p : Point n) : Fin (2 * n - 1) :=
+  ⟨p.1.1 + (n - 1 - p.2.1), by omega⟩
+
+structure FourWeights (n : ℕ) where
+  row : Fin n → ℚ
+  column : Fin n → ℚ
+  sum : Fin (2 * n - 1) → ℚ
+  difference : Fin (2 * n - 1) → ℚ
+
+def fourCoverage {n : ℕ} (w : FourWeights n) (p : Point n) : ℚ :=
+  w.row p.1 + w.column p.2 + w.sum (sumIndex p) +
+    w.difference (differenceIndex p)
+
+def fourCost {n : ℕ} (w : FourWeights n) : ℚ :=
+  2 * ((∑ i, w.row i) + (∑ i, w.column i) +
+    (∑ i, w.sum i) + ∑ i, w.difference i)
+
+private theorem fiberCard_le_two_of_collinear
+    {n : ℕ} {β : Type*} [DecidableEq β]
+    {s : Finset (Point n)} (hntil : NoThreeInLine s)
+    (f : Point n → β)
+    (hcollinear : ∀ {a b c : Point n},
+      f a = f b → f a = f c → determinant a b c = 0)
+    (value : β) : fiberCard s f value ≤ 2 := by
+  change (s.filter fun p => f p = value).card ≤ 2
+  by_contra h
+  have hthree : 2 < (s.filter fun p => f p = value).card :=
+    Nat.lt_of_not_ge h
+  obtain ⟨a, ha, b, hb, c, hc, hab, hac, hbc⟩ :=
+    Finset.two_lt_card.mp hthree
+  have haS : a ∈ s := (Finset.mem_filter.mp ha).1
+  have hbS : b ∈ s := (Finset.mem_filter.mp hb).1
+  have hcS : c ∈ s := (Finset.mem_filter.mp hc).1
+  have haf : f a = value := (Finset.mem_filter.mp ha).2
+  have hbf : f b = value := (Finset.mem_filter.mp hb).2
+  have hcf : f c = value := (Finset.mem_filter.mp hc).2
+  have hab' : (⟨a, haS⟩ : ↥s) ≠ ⟨b, hbS⟩ := by
+    intro e
+    exact hab (congrArg Subtype.val e)
+  have hac' : (⟨a, haS⟩ : ↥s) ≠ ⟨c, hcS⟩ := by
+    intro e
+    exact hac (congrArg Subtype.val e)
+  have hbc' : (⟨b, hbS⟩ : ↥s) ≠ ⟨c, hcS⟩ := by
+    intro e
+    exact hbc (congrArg Subtype.val e)
+  exact hntil ⟨a, haS⟩ ⟨b, hbS⟩ ⟨c, hcS⟩ hab' hac' hbc'
+    (hcollinear (haf.trans hbf.symm) (haf.trans hcf.symm))
+
+theorem rowFiber_le_two {n : ℕ} {s : Finset (Point n)}
+    (hntil : NoThreeInLine s) (i : Fin n) :
+    fiberCard s (fun p : Point n => p.1) i ≤ 2 := by
+  apply fiberCard_le_two_of_collinear hntil (fun p : Point n => p.1)
+  intro a b c hab hac
+  have hb : b.1 = a.1 := hab.symm
+  have hc : c.1 = a.1 := hac.symm
+  simp [determinant, hb, hc]
+
+theorem columnFiber_le_two {n : ℕ} {s : Finset (Point n)}
+    (hntil : NoThreeInLine s) (i : Fin n) :
+    fiberCard s (fun p : Point n => p.2) i ≤ 2 := by
+  apply fiberCard_le_two_of_collinear hntil (fun p : Point n => p.2)
+  intro a b c hab hac
+  have hb : b.2 = a.2 := hab.symm
+  have hc : c.2 = a.2 := hac.symm
+  simp [determinant, hb, hc]
+
+theorem sumFiber_le_two {n : ℕ} {s : Finset (Point n)}
+    (hntil : NoThreeInLine s) (i : Fin (2 * n - 1)) :
+    fiberCard s sumIndex i ≤ 2 := by
+  apply fiberCard_le_two_of_collinear hntil sumIndex
+  intro a b c hab hac
+  have habv : a.1.1 + a.2.1 = b.1.1 + b.2.1 := congrArg Fin.val hab
+  have hacv : a.1.1 + a.2.1 = c.1.1 + c.2.1 := congrArg Fin.val hac
+  have habz : (a.1.1 : ℤ) + a.2.1 = (b.1.1 : ℤ) + b.2.1 := by
+    exact_mod_cast habv
+  have hacz : (a.1.1 : ℤ) + a.2.1 = (c.1.1 : ℤ) + c.2.1 := by
+    exact_mod_cast hacv
+  have hb : (b.2.1 : ℤ) - a.2.1 = -((b.1.1 : ℤ) - a.1.1) := by
+    linarith
+  have hc : (c.2.1 : ℤ) - a.2.1 = -((c.1.1 : ℤ) - a.1.1) := by
+    linarith
+  rw [determinant, hb, hc]
+  ring
+
+theorem differenceFiber_le_two {n : ℕ} {s : Finset (Point n)}
+    (hntil : NoThreeInLine s) (i : Fin (2 * n - 1)) :
+    fiberCard s differenceIndex i ≤ 2 := by
+  apply fiberCard_le_two_of_collinear hntil differenceIndex
+  intro a b c hab hac
+  have habv :
+      a.1.1 + (n - 1 - a.2.1) = b.1.1 + (n - 1 - b.2.1) :=
+    congrArg Fin.val hab
+  have hacv :
+      a.1.1 + (n - 1 - a.2.1) = c.1.1 + (n - 1 - c.2.1) :=
+    congrArg Fin.val hac
+  have habn : a.1.1 + b.2.1 = b.1.1 + a.2.1 := by omega
+  have hacn : a.1.1 + c.2.1 = c.1.1 + a.2.1 := by omega
+  have habz : (a.1.1 : ℤ) + b.2.1 = (b.1.1 : ℤ) + a.2.1 := by
+    exact_mod_cast habn
+  have hacz : (a.1.1 : ℤ) + c.2.1 = (c.1.1 : ℤ) + a.2.1 := by
+    exact_mod_cast hacn
+  have hb : (b.2.1 : ℤ) - a.2.1 = (b.1.1 : ℤ) - a.1.1 := by
+    linarith
+  have hc : (c.2.1 : ℤ) - a.2.1 = (c.1.1 : ℤ) - a.1.1 := by
+    linarith
+  rw [determinant, hb, hc]
+  ring
+
+private theorem weightedFibers_le_two
+    {α β : Type*} [DecidableEq α] [DecidableEq β] [Fintype β]
+    (s : Finset α) (f : α → β) (weight : β → ℚ)
+    (hweight : ∀ i, 0 ≤ weight i)
+    (hcard : ∀ i, fiberCard s f i ≤ 2) :
+    (∑ i, (fiberCard s f i : ℚ) * weight i) ≤ 2 * ∑ i, weight i := by
+  rw [Finset.mul_sum]
+  apply Finset.sum_le_sum
+  intro i _
+  have hi : (fiberCard s f i : ℚ) ≤ 2 := by
+    exact_mod_cast hcard i
+  nlinarith [hweight i]
+
+theorem fourCertificate_bound {n : ℕ} {s : Finset (Point n)}
+    (w : FourWeights n)
+    (hrow : ∀ i, 0 ≤ w.row i)
+    (hcolumn : ∀ i, 0 ≤ w.column i)
+    (hsum : ∀ i, 0 ≤ w.sum i)
+    (hdifference : ∀ i, 0 ≤ w.difference i)
+    (hntil : NoThreeInLine s) :
+    (∑ p ∈ s, fourCoverage w p) ≤ fourCost w := by
+  have hr : (∑ p ∈ s, w.row p.1) ≤ 2 * ∑ i, w.row i := by
+    rw [← sum_fiberCard_mul (R := ℚ) s (fun p : Point n => p.1) w.row]
+    exact weightedFibers_le_two s (fun p : Point n => p.1) w.row hrow
+      (rowFiber_le_two hntil)
+  have hc : (∑ p ∈ s, w.column p.2) ≤ 2 * ∑ i, w.column i := by
+    rw [← sum_fiberCard_mul (R := ℚ) s (fun p : Point n => p.2) w.column]
+    exact weightedFibers_le_two s (fun p : Point n => p.2) w.column hcolumn
+      (columnFiber_le_two hntil)
+  have hs : (∑ p ∈ s, w.sum (sumIndex p)) ≤ 2 * ∑ i, w.sum i := by
+    rw [← sum_fiberCard_mul (R := ℚ) s sumIndex w.sum]
+    exact weightedFibers_le_two s sumIndex w.sum hsum (sumFiber_le_two hntil)
+  have hd : (∑ p ∈ s, w.difference (differenceIndex p)) ≤ 2 * ∑ i, w.difference i := by
+    rw [← sum_fiberCard_mul (R := ℚ) s differenceIndex w.difference]
+    exact weightedFibers_le_two s differenceIndex w.difference hdifference
+      (differenceFiber_le_two hntil)
+  calc
+    (∑ p ∈ s, fourCoverage w p) =
+        (∑ p ∈ s, w.row p.1) + (∑ p ∈ s, w.column p.2) +
+          (∑ p ∈ s, w.sum (sumIndex p)) +
+            ∑ p ∈ s, w.difference (differenceIndex p) := by
+              simp [fourCoverage, Finset.sum_add_distrib, add_assoc]
+    _ ≤ 2 * (∑ i, w.row i) + 2 * (∑ i, w.column i) +
+          2 * (∑ i, w.sum i) + 2 * ∑ i, w.difference i := by
+            linarith
+    _ = fourCost w := by
+      simp [fourCost]
+      ring
+
+theorem card_le_of_fourCertificate {n k : ℕ} {q : ℚ}
+    {s : Finset (Point n)} (w : FourWeights n)
+    (hq : 0 < q)
+    (hcost : fourCost w < q * (k + 1))
+    (hrow : ∀ i, 0 ≤ w.row i)
+    (hcolumn : ∀ i, 0 ≤ w.column i)
+    (hsum : ∀ i, 0 ≤ w.sum i)
+    (hdifference : ∀ i, 0 ≤ w.difference i)
+    (hcover : ∀ p : ↥s, q ≤ fourCoverage w p.1)
+    (hntil : NoThreeInLine s) : s.card ≤ k := by
+  have hlower : q * (s.card : ℚ) ≤ ∑ p ∈ s, fourCoverage w p := by
+    calc
+      q * (s.card : ℚ) = ∑ _p ∈ s, q := by simp [mul_comm]
+      _ ≤ ∑ p ∈ s, fourCoverage w p := by
+        apply Finset.sum_le_sum
+        intro p hp
+        exact hcover ⟨p, hp⟩
+  have hupper := fourCertificate_bound w hrow hcolumn hsum hdifference hntil
+  have hltQ : (s.card : ℚ) < k + 1 := by nlinarith
+  have hltN : s.card < k + 1 := by exact_mod_cast hltQ
+  omega
+
+end Checkerboard
diff --git a/Checkerboard/Model.lean b/Checkerboard/Model.lean
new file mode 100644
index 00000000..08af06af
--- /dev/null
+++ b/Checkerboard/Model.lean
@@ -0,0 +1,165 @@
+import Mathlib
+
+namespace Checkerboard
+
+abbrev Point (n : ℕ) := Fin n × Fin n
+
+def determinant {n : ℕ} (a b c : Point n) : ℤ :=
+  ((b.1.1 : ℤ) - (a.1.1 : ℤ)) * ((c.2.1 : ℤ) - (a.2.1 : ℤ)) -
+    ((b.2.1 : ℤ) - (a.2.1 : ℤ)) * ((c.1.1 : ℤ) - (a.1.1 : ℤ))
+
+def InColor {n : ℕ} (parity : ℕ) (p : Point n) : Prop :=
+  (p.1.1 + p.2.1) % 2 = parity % 2
+
+def Monochromatic {n : ℕ} (parity : ℕ) (s : Finset (Point n)) : Prop :=
+  ∀ p : ↥s, InColor parity p.1
+
+def NoThreeInLine {n : ℕ} (s : Finset (Point n)) : Prop :=
+  ∀ a b c : ↥s, a ≠ b → a ≠ c → b ≠ c →
+    determinant a.1 b.1 c.1 ≠ 0
+
+def IsExactMaximum (n parity k : ℕ) : Prop :=
+  (∃ s : Finset (Point n),
+      Monochromatic parity s ∧ NoThreeInLine s ∧ s.card = k) ∧
+    ∀ s : Finset (Point n),
+      Monochromatic parity s → NoThreeInLine s → s.card ≤ k
+
+inductive LineFamily
+  | row | column | sum | difference
+  deriving DecidableEq, Fintype, Repr
+
+abbrev PrincipalLine (n : ℕ) := LineFamily × Fin (2 * n - 1)
+
+def lineValue {n : ℕ} (family : LineFamily) (p : Point n) : ℤ :=
+  match family with
+  | .row => p.1.1
+  | .column => p.2.1
+  | .sum => p.1.1 + p.2.1
+  | .difference => (p.1.1 : ℤ) - (p.2.1 : ℤ) + (n - 1 : ℕ)
+
+def OnLine {n : ℕ} (line : PrincipalLine n) (p : Point n) : Prop :=
+  lineValue line.1 p = line.2.1
+
+instance {n : ℕ} (line : PrincipalLine n) : DecidablePred (OnLine line) := by
+  intro p
+  unfold OnLine
+  infer_instance
+
+theorem principal_collinear {n : ℕ} {line : PrincipalLine n}
+    {a b c : Point n} (ha : OnLine line a) (hb : OnLine line b)
+    (hc : OnLine line c) : determinant a b c = 0 := by
+  rcases line with ⟨family, index⟩
+  cases family with
+  | row =>
+      simp only [OnLine, lineValue] at ha hb hc
+      simp [determinant, ha, hb, hc]
+  | column =>
+      simp only [OnLine, lineValue] at ha hb hc
+      simp [determinant, ha, hb, hc]
+  | sum =>
+      simp only [OnLine, lineValue] at ha hb hc
+      have hba : ((b.2.1 : ℤ) - (a.2.1 : ℤ)) = -((b.1.1 : ℤ) - (a.1.1 : ℤ)) := by linarith
+      have hca : ((c.2.1 : ℤ) - (a.2.1 : ℤ)) = -((c.1.1 : ℤ) - (a.1.1 : ℤ)) := by linarith
+      rw [determinant, hba, hca]
+      ring
+  | difference =>
+      simp only [OnLine, lineValue] at ha hb hc
+      have hba : ((b.2.1 : ℤ) - (a.2.1 : ℤ)) = ((b.1.1 : ℤ) - (a.1.1 : ℤ)) := by linarith
+      have hca : ((c.2.1 : ℤ) - (a.2.1 : ℤ)) = ((c.1.1 : ℤ) - (a.1.1 : ℤ)) := by linarith
+      rw [determinant, hba, hca]
+      ring
+
+theorem principalLine_card_le_two {n : ℕ} {s : Finset (Point n)}
+    (hntil : NoThreeInLine s) (line : PrincipalLine n) :
+    (s.filter (OnLine line)).card ≤ 2 := by
+  by_contra h
+  have hthree : 2 < (s.filter (OnLine line)).card := Nat.lt_of_not_ge h
+  obtain ⟨a, ha, b, hb, c, hc, hab, hac, hbc⟩ := Finset.two_lt_card.mp hthree
+  have haS := (Finset.mem_filter.mp ha).1
+  have hbS := (Finset.mem_filter.mp hb).1
+  have hcS := (Finset.mem_filter.mp hc).1
+  have haL := (Finset.mem_filter.mp ha).2
+  have hbL := (Finset.mem_filter.mp hb).2
+  have hcL := (Finset.mem_filter.mp hc).2
+  have hab' : (⟨a, haS⟩ : ↥s) ≠ ⟨b, hbS⟩ := by intro e; exact hab (congrArg Subtype.val e)
+  have hac' : (⟨a, haS⟩ : ↥s) ≠ ⟨c, hcS⟩ := by intro e; exact hac (congrArg Subtype.val e)
+  have hbc' : (⟨b, hbS⟩ : ↥s) ≠ ⟨c, hcS⟩ := by intro e; exact hbc (congrArg Subtype.val e)
+  exact hntil ⟨a, haS⟩ ⟨b, hbS⟩ ⟨c, hcS⟩ hab' hac' hbc'
+    (principal_collinear haL hbL hcL)
+
+def coverage {n : ℕ} (weight : PrincipalLine n → ℕ) (p : Point n) : ℕ :=
+  ∑ line : PrincipalLine n, if OnLine line p then weight line else 0
+
+def certificateCost {n : ℕ} (weight : PrincipalLine n → ℕ) : ℕ :=
+  ∑ line : PrincipalLine n, 2 * weight line
+
+private theorem sum_indicator_eq_card_filter {α : Type*} [DecidableEq α]
+    (s : Finset α) (P : α → Prop) [DecidablePred P] (w : ℕ) :
+    (∑ a ∈ s, if P a then w else 0) = (s.filter P).card * w := by
+  induction s using Finset.induction_on with
+  | empty => simp
+  | @insert a s ha ih =>
+      by_cases hP : P a
+      · have hnot : a ∉ s.filter P := by
+          intro hmem
+          exact ha (Finset.mem_filter.mp hmem).1
+        have hfilter : (insert a s).filter P = insert a (s.filter P) := by
+          ext x
+          by_cases hxa : x = a
+          · subst x; simp [ha, hP]
+          · simp [hxa]
+        rw [Finset.sum_insert ha, if_pos hP, hfilter, ih]
+        simp [hnot, Nat.add_mul, Nat.add_comm]
+      · have hfilter : (insert a s).filter P = s.filter P := by
+          ext x
+          by_cases hxa : x = a
+          · subst x; simp [ha, hP]
+          · simp [hxa]
+        rw [Finset.sum_insert ha, if_neg hP, hfilter, ih]
+        simp
+
+private theorem double_count {n : ℕ} (s : Finset (Point n))
+    (weight : PrincipalLine n → ℕ) :
+    (∑ p ∈ s, coverage weight p) =
+      ∑ line : PrincipalLine n, (s.filter (OnLine line)).card * weight line := by
+  calc
+    (∑ p ∈ s, coverage weight p) =
+        ∑ p ∈ s, ∑ line : PrincipalLine n, if OnLine line p then weight line else 0 := by rfl
+    _ = ∑ line : PrincipalLine n, ∑ p ∈ s, if OnLine line p then weight line else 0 := by
+      rw [Finset.sum_comm]
+    _ = ∑ line : PrincipalLine n, (s.filter (OnLine line)).card * weight line := by
+      apply Finset.sum_congr rfl
+      intro line _
+      exact sum_indicator_eq_card_filter s (OnLine line) (weight line)
+
+theorem certificate_bound {n q : ℕ} {s : Finset (Point n)}
+    (weight : PrincipalLine n → ℕ)
+    (hcover : ∀ p : ↥s, q ≤ coverage weight p.1)
+    (hntil : NoThreeInLine s) : q * s.card ≤ certificateCost weight := by
+  have hpoint : (∑ p ∈ s, q) ≤ ∑ p ∈ s, coverage weight p := by
+    apply Finset.sum_le_sum
+    intro p hp
+    exact hcover ⟨p, hp⟩
+  have hline :
+      (∑ line : PrincipalLine n, (s.filter (OnLine line)).card * weight line) ≤
+        certificateCost weight := by
+    apply Finset.sum_le_sum
+    intro line _
+    exact Nat.mul_le_mul_right (weight line) (principalLine_card_le_two hntil line)
+  calc
+    q * s.card = ∑ _p ∈ s, q := by simp [Nat.mul_comm]
+    _ ≤ ∑ p ∈ s, coverage weight p := hpoint
+    _ = ∑ line : PrincipalLine n, (s.filter (OnLine line)).card * weight line := double_count s weight
+    _ ≤ certificateCost weight := hline
+
+theorem card_le_of_certificate {n parity q k : ℕ} {s : Finset (Point n)}
+    (weight : PrincipalLine n → ℕ) (hq : 0 < q)
+    (hcost : certificateCost weight < q * (k + 1))
+    (hglobal : ∀ p : Point n, InColor parity p → q ≤ coverage weight p)
+    (hcolor : Monochromatic parity s) (hntil : NoThreeInLine s) : s.card ≤ k := by
+  have hb := certificate_bound weight (fun p => hglobal p.1 (hcolor p)) hntil
+  have hmul : q * s.card < q * (k + 1) := lt_of_le_of_lt hb hcost
+  have hlt : s.card < k + 1 := (Nat.mul_lt_mul_left hq).mp hmul
+  omega
+
+end Checkerboard
diff --git a/Checkerboard/N6Base.lean b/Checkerboard/N6Base.lean
new file mode 100644
index 00000000..38074303
--- /dev/null
+++ b/Checkerboard/N6Base.lean
@@ -0,0 +1,258 @@
+import Checkerboard.FourCertificate
+import Checkerboard.N6SATTest
+
+/-!
+# The final 6×6 base cases
+
+The uniform quadratic cover does not exclude nine points on the 6-board, so an
+integrality argument is required. Each color class has eighteen points. We
+transport an arbitrary monochromatic set to eighteen Boolean variables, derive
+explicit row, column, and slope `±1` capacity inequalities, and discharge the
+resulting Presburger certificates with `omega`.
+
+Proof developed by Dominic Dabish. ProofOrchestrator, using OpenAI GPT-5.6 Thinking,
+assisted with the mathematical argument, Lean formalization, and submission
+preparation. All formal claims are checked by the repository-pinned Lean compiler.
+-/
+
+namespace Checkerboard
+
+set_option maxHeartbeats 0
+set_option maxRecDepth 1000000
+
+/-- Enumeration of the fat color class of the 6-board. -/
+def n6p0Point : Fin 18 → Point 6 := ![
+  ((0 : Fin 6), (0 : Fin 6)), ((0 : Fin 6), (2 : Fin 6)),
+  ((0 : Fin 6), (4 : Fin 6)), ((1 : Fin 6), (1 : Fin 6)),
+  ((1 : Fin 6), (3 : Fin 6)), ((1 : Fin 6), (5 : Fin 6)),
+  ((2 : Fin 6), (0 : Fin 6)), ((2 : Fin 6), (2 : Fin 6)),
+  ((2 : Fin 6), (4 : Fin 6)), ((3 : Fin 6), (1 : Fin 6)),
+  ((3 : Fin 6), (3 : Fin 6)), ((3 : Fin 6), (5 : Fin 6)),
+  ((4 : Fin 6), (0 : Fin 6)), ((4 : Fin 6), (2 : Fin 6)),
+  ((4 : Fin 6), (4 : Fin 6)), ((5 : Fin 6), (1 : Fin 6)),
+  ((5 : Fin 6), (3 : Fin 6)), ((5 : Fin 6), (5 : Fin 6))]
+
+/-- Enumeration of the thin color class of the 6-board. -/
+def n6p1Point : Fin 18 → Point 6 := ![
+  ((0 : Fin 6), (1 : Fin 6)), ((0 : Fin 6), (3 : Fin 6)),
+  ((0 : Fin 6), (5 : Fin 6)), ((1 : Fin 6), (0 : Fin 6)),
+  ((1 : Fin 6), (2 : Fin 6)), ((1 : Fin 6), (4 : Fin 6)),
+  ((2 : Fin 6), (1 : Fin 6)), ((2 : Fin 6), (3 : Fin 6)),
+  ((2 : Fin 6), (5 : Fin 6)), ((3 : Fin 6), (0 : Fin 6)),
+  ((3 : Fin 6), (2 : Fin 6)), ((3 : Fin 6), (4 : Fin 6)),
+  ((4 : Fin 6), (1 : Fin 6)), ((4 : Fin 6), (3 : Fin 6)),
+  ((4 : Fin 6), (5 : Fin 6)), ((5 : Fin 6), (0 : Fin 6)),
+  ((5 : Fin 6), (2 : Fin 6)), ((5 : Fin 6), (4 : Fin 6))]
+
+private theorem n6p0_injective : Function.Injective n6p0Point := by decide
+private theorem n6p1_injective : Function.Injective n6p1Point := by decide
+
+private theorem n6p0_surjective :
+    ∀ p : Point 6, InColor 0 p → ∃ i, n6p0Point i = p := by
+  letI : DecidablePred (fun p : Point 6 =>
+      InColor 0 p → ∃ i, n6p0Point i = p) := by
+    intro p
+    unfold InColor
+    infer_instance
+  exact of_decide_eq_true rfl
+
+private theorem n6p1_surjective :
+    ∀ p : Point 6, InColor 1 p → ∃ i, n6p1Point i = p := by
+  letI : DecidablePred (fun p : Point 6 =>
+      InColor 1 p → ∃ i, n6p1Point i = p) := by
+    intro p
+    unfold InColor
+    infer_instance
+  exact of_decide_eq_true rfl
+
+private def chosenIndices (point : Fin 18 → Point 6)
+    (s : Finset (Point 6)) : Finset (Fin 18) :=
+  Finset.univ.filter fun i => point i ∈ s
+
+private def chosenOnLine (point : Fin 18 → Point 6)
+    (s : Finset (Point 6)) (line : PrincipalLine 6) : Finset (Fin 18) :=
+  Finset.univ.filter fun i => point i ∈ s ∧ OnLine line (point i)
+
+private theorem card_filter_bool {α : Type*} (s : Finset α) (x : α → Bool) :
+    (s.filter fun i => x i = true).card =
+      Finset.sum s (fun i => bitNat (x i)) := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | @insert a s ha ih =>
+      cases hxa : x a <;> simp [ha, ih, hxa, bitNat]
+
+private theorem card_filter_bool_and {α : Type*} (s : Finset α)
+    (x : α → Bool) (p : α → Prop) [DecidablePred p] :
+    (s.filter fun i => x i = true ∧ p i).card =
+      Finset.sum (s.filter p) (fun i => bitNat (x i)) := by
+  classical
+  have hfilter :
+      s.filter (fun i => x i = true ∧ p i) =
+        (s.filter p).filter (fun i => x i = true) := by
+    ext i
+    simp [and_comm]
+  rw [hfilter]
+  exact card_filter_bool (s.filter p) x
+
+private theorem chosenIndices_image
+    {parity : ℕ} (point : Fin 18 → Point 6)
+    (hsurj : ∀ p : Point 6, InColor parity p → ∃ i, point i = p)
+    (s : Finset (Point 6)) (hcolor : Monochromatic parity s) :
+    (chosenIndices point s).image point = s := by
+  ext p
+  constructor
+  · intro hp
+    rcases Finset.mem_image.mp hp with ⟨i, hi, rfl⟩
+    exact (Finset.mem_filter.mp hi).2
+  · intro hp
+    obtain ⟨i, hi⟩ := hsurj p (hcolor ⟨p, hp⟩)
+    subst p
+    apply Finset.mem_image.mpr
+    exact ⟨i, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hp⟩, rfl⟩
+
+private theorem chosenOnLine_image
+    {parity : ℕ} (point : Fin 18 → Point 6)
+    (hsurj : ∀ p : Point 6, InColor parity p → ∃ i, point i = p)
+    (s : Finset (Point 6)) (hcolor : Monochromatic parity s)
+    (line : PrincipalLine 6) :
+    (chosenOnLine point s line).image point = s.filter (OnLine line) := by
+  ext p
+  constructor
+  · intro hp
+    rcases Finset.mem_image.mp hp with ⟨i, hi, rfl⟩
+    exact Finset.mem_filter.mpr (Finset.mem_filter.mp hi).2
+  · intro hp
+    have hpS := (Finset.mem_filter.mp hp).1
+    have hpL := (Finset.mem_filter.mp hp).2
+    obtain ⟨i, hi⟩ := hsurj p (hcolor ⟨p, hpS⟩)
+    subst p
+    apply Finset.mem_image.mpr
+    exact ⟨i, Finset.mem_filter.mpr
+      ⟨Finset.mem_univ _, ⟨hpS, hpL⟩⟩, rfl⟩
+
+private theorem upper_of_boolean_certificate
+    {parity : ℕ} (point : Fin 18 → Point 6)
+    (hinj : Function.Injective point)
+    (hsurj : ∀ p : Point 6, InColor parity p → ∃ i, point i = p)
+    (hfinite : ∀ x : Fin 18 → Bool,
+      (∀ line : PrincipalLine 6,
+        (Finset.univ.filter fun i => x i = true ∧ OnLine line (point i)).card ≤ 2) →
+      (Finset.univ.filter fun i => x i = true).card ≤ 8)
+    (s : Finset (Point 6))
+    (hcolor : Monochromatic parity s) (hntil : NoThreeInLine s) :
+    s.card ≤ 8 := by
+  let x : Fin 18 → Bool := fun i => decide (point i ∈ s)
+  have hline : ∀ line : PrincipalLine 6,
+      (Finset.univ.filter fun i => x i = true ∧ OnLine line (point i)).card ≤ 2 := by
+    intro line
+    have himage := chosenOnLine_image point hsurj s hcolor line
+    have hcardImage := Finset.card_image_of_injective
+      (chosenOnLine point s line) hinj
+    have hchosen :
+        (chosenOnLine point s line).card = (s.filter (OnLine line)).card := by
+      calc
+        (chosenOnLine point s line).card =
+            ((chosenOnLine point s line).image point).card := hcardImage.symm
+        _ = (s.filter (OnLine line)).card := congrArg Finset.card himage
+    have heq :
+        (Finset.univ.filter fun i => x i = true ∧ OnLine line (point i)).card =
+          (s.filter (OnLine line)).card := by
+      simpa [x, chosenOnLine] using hchosen
+    rw [heq]
+    exact principalLine_card_le_two hntil line
+  have hbool := hfinite x hline
+  have himage := chosenIndices_image point hsurj s hcolor
+  have hcardImage := Finset.card_image_of_injective (chosenIndices point s) hinj
+  have hchosen : (chosenIndices point s).card = s.card := by
+    calc
+      (chosenIndices point s).card = ((chosenIndices point s).image point).card :=
+        hcardImage.symm
+      _ = s.card := congrArg Finset.card himage
+  have heq : (Finset.univ.filter fun i => x i = true).card = s.card := by
+    simpa [x, chosenIndices] using hchosen
+  rwa [heq] at hbool
+
+private theorem n6p0_boolean_bound :
+    ∀ x : Fin 18 → Bool,
+      (∀ line : PrincipalLine 6,
+        (Finset.univ.filter fun i =>
+          x i = true ∧ OnLine line (n6p0Point i)).card ≤ 2) →
+      (Finset.univ.filter fun i => x i = true).card ≤ 8 := by
+  intro x hline
+  have h0 := hline (LineFamily.row, ⟨0, by decide⟩)
+  have h1 := hline (LineFamily.row, ⟨1, by decide⟩)
+  have h2 := hline (LineFamily.row, ⟨2, by decide⟩)
+  have h3 := hline (LineFamily.row, ⟨3, by decide⟩)
+  have h4 := hline (LineFamily.row, ⟨4, by decide⟩)
+  have h5 := hline (LineFamily.row, ⟨5, by decide⟩)
+  have h6 := hline (LineFamily.column, ⟨0, by decide⟩)
+  have h7 := hline (LineFamily.column, ⟨2, by decide⟩)
+  have h8 := hline (LineFamily.column, ⟨4, by decide⟩)
+  have h9 := hline (LineFamily.column, ⟨1, by decide⟩)
+  have h10 := hline (LineFamily.column, ⟨3, by decide⟩)
+  have h11 := hline (LineFamily.column, ⟨5, by decide⟩)
+  have h12 := hline (LineFamily.sum, ⟨2, by decide⟩)
+  have h13 := hline (LineFamily.sum, ⟨4, by decide⟩)
+  have h14 := hline (LineFamily.sum, ⟨6, by decide⟩)
+  have h15 := hline (LineFamily.sum, ⟨8, by decide⟩)
+  have h16 := hline (LineFamily.difference, ⟨5, by decide⟩)
+  have h17 := hline (LineFamily.difference, ⟨3, by decide⟩)
+  have h18 := hline (LineFamily.difference, ⟨7, by decide⟩)
+  rw [card_filter_bool_and] at h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18
+  norm_num [n6p0Point, OnLine, lineValue] at h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18
+  rw [card_filter_bool]
+  norm_num
+  exact n6p0_sat (x 0) (x 1) (x 2) (x 3) (x 4) (x 5)
+    (x 6) (x 7) (x 8) (x 9) (x 10) (x 11)
+    (x 12) (x 13) (x 14) (x 15) (x 16) (x 17)
+    h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18
+
+private theorem n6p1_boolean_bound :
+    ∀ x : Fin 18 → Bool,
+      (∀ line : PrincipalLine 6,
+        (Finset.univ.filter fun i =>
+          x i = true ∧ OnLine line (n6p1Point i)).card ≤ 2) →
+      (Finset.univ.filter fun i => x i = true).card ≤ 8 := by
+  intro x hline
+  have h0 := hline (LineFamily.row, ⟨0, by decide⟩)
+  have h1 := hline (LineFamily.row, ⟨1, by decide⟩)
+  have h2 := hline (LineFamily.row, ⟨2, by decide⟩)
+  have h3 := hline (LineFamily.row, ⟨3, by decide⟩)
+  have h4 := hline (LineFamily.row, ⟨4, by decide⟩)
+  have h5 := hline (LineFamily.row, ⟨5, by decide⟩)
+  have h6 := hline (LineFamily.column, ⟨1, by decide⟩)
+  have h7 := hline (LineFamily.column, ⟨3, by decide⟩)
+  have h8 := hline (LineFamily.column, ⟨5, by decide⟩)
+  have h9 := hline (LineFamily.column, ⟨0, by decide⟩)
+  have h10 := hline (LineFamily.column, ⟨2, by decide⟩)
+  have h11 := hline (LineFamily.column, ⟨4, by decide⟩)
+  have h12 := hline (LineFamily.sum, ⟨3, by decide⟩)
+  have h13 := hline (LineFamily.sum, ⟨5, by decide⟩)
+  have h14 := hline (LineFamily.sum, ⟨7, by decide⟩)
+  have h15 := hline (LineFamily.difference, ⟨4, by decide⟩)
+  have h16 := hline (LineFamily.difference, ⟨2, by decide⟩)
+  have h17 := hline (LineFamily.difference, ⟨6, by decide⟩)
+  have h18 := hline (LineFamily.difference, ⟨8, by decide⟩)
+  rw [card_filter_bool_and] at h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18
+  norm_num [n6p1Point, OnLine, lineValue] at h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18
+  rw [card_filter_bool]
+  norm_num
+  exact n6p1_sat (x 0) (x 1) (x 2) (x 3) (x 4) (x 5)
+    (x 6) (x 7) (x 8) (x 9) (x 10) (x 11)
+    (x 12) (x 13) (x 14) (x 15) (x 16) (x 17)
+    h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18
+
+/-- `D_mono(6,0) ≤ 8`. -/
+theorem n6_zero_upper (s : Finset (Point 6))
+    (hcolor : Monochromatic 0 s) (hntil : NoThreeInLine s) : s.card ≤ 8 := by
+  exact upper_of_boolean_certificate n6p0Point n6p0_injective n6p0_surjective
+    n6p0_boolean_bound s hcolor hntil
+
+/-- `D_mono(6,1) ≤ 8`. -/
+theorem n6_one_upper (s : Finset (Point 6))
+    (hcolor : Monochromatic 1 s) (hntil : NoThreeInLine s) : s.card ≤ 8 := by
+  exact upper_of_boolean_certificate n6p1Point n6p1_injective n6p1_surjective
+    n6p1_boolean_bound s hcolor hntil
+
+end Checkerboard
diff --git a/Checkerboard/N6BridgeTest.lean b/Checkerboard/N6BridgeTest.lean
new file mode 100644
index 00000000..d7f00cc7
--- /dev/null
+++ b/Checkerboard/N6BridgeTest.lean
@@ -0,0 +1,91 @@
+import Checkerboard.FourCertificate
+import Checkerboard.N6SATTest
+
+namespace Checkerboard
+
+private def p0Point : Fin 18 → Point 6 := ![
+  ((0 : Fin 6), (0 : Fin 6)), ((0 : Fin 6), (2 : Fin 6)),
+  ((0 : Fin 6), (4 : Fin 6)), ((1 : Fin 6), (1 : Fin 6)),
+  ((1 : Fin 6), (3 : Fin 6)), ((1 : Fin 6), (5 : Fin 6)),
+  ((2 : Fin 6), (0 : Fin 6)), ((2 : Fin 6), (2 : Fin 6)),
+  ((2 : Fin 6), (4 : Fin 6)), ((3 : Fin 6), (1 : Fin 6)),
+  ((3 : Fin 6), (3 : Fin 6)), ((3 : Fin 6), (5 : Fin 6)),
+  ((4 : Fin 6), (0 : Fin 6)), ((4 : Fin 6), (2 : Fin 6)),
+  ((4 : Fin 6), (4 : Fin 6)), ((5 : Fin 6), (1 : Fin 6)),
+  ((5 : Fin 6), (3 : Fin 6)), ((5 : Fin 6), (5 : Fin 6))]
+
+private def p1Point : Fin 18 → Point 6 := ![
+  ((0 : Fin 6), (1 : Fin 6)), ((0 : Fin 6), (3 : Fin 6)),
+  ((0 : Fin 6), (5 : Fin 6)), ((1 : Fin 6), (0 : Fin 6)),
+  ((1 : Fin 6), (2 : Fin 6)), ((1 : Fin 6), (4 : Fin 6)),
+  ((2 : Fin 6), (1 : Fin 6)), ((2 : Fin 6), (3 : Fin 6)),
+  ((2 : Fin 6), (5 : Fin 6)), ((3 : Fin 6), (0 : Fin 6)),
+  ((3 : Fin 6), (2 : Fin 6)), ((3 : Fin 6), (4 : Fin 6)),
+  ((4 : Fin 6), (1 : Fin 6)), ((4 : Fin 6), (3 : Fin 6)),
+  ((4 : Fin 6), (5 : Fin 6)), ((5 : Fin 6), (0 : Fin 6)),
+  ((5 : Fin 6), (2 : Fin 6)), ((5 : Fin 6), (4 : Fin 6))]
+
+private theorem p0_bridge
+    (x : Fin 18 → Bool)
+    (hline : ∀ line : PrincipalLine 6,
+      (Finset.univ.filter fun i => x i = true ∧ OnLine line (p0Point i)).card ≤ 2) :
+    (Finset.univ.filter fun i => x i = true).card ≤ 8 := by
+  have h0 := hline (LineFamily.row, ⟨0, by decide⟩)
+  have h1 := hline (LineFamily.row, ⟨1, by decide⟩)
+  have h2 := hline (LineFamily.row, ⟨2, by decide⟩)
+  have h3 := hline (LineFamily.row, ⟨3, by decide⟩)
+  have h4 := hline (LineFamily.row, ⟨4, by decide⟩)
+  have h5 := hline (LineFamily.row, ⟨5, by decide⟩)
+  have h6 := hline (LineFamily.column, ⟨0, by decide⟩)
+  have h7 := hline (LineFamily.column, ⟨2, by decide⟩)
+  have h8 := hline (LineFamily.column, ⟨4, by decide⟩)
+  have h9 := hline (LineFamily.column, ⟨1, by decide⟩)
+  have h10 := hline (LineFamily.column, ⟨3, by decide⟩)
+  have h11 := hline (LineFamily.column, ⟨5, by decide⟩)
+  have h12 := hline (LineFamily.sum, ⟨2, by decide⟩)
+  have h13 := hline (LineFamily.sum, ⟨4, by decide⟩)
+  have h14 := hline (LineFamily.sum, ⟨6, by decide⟩)
+  have h15 := hline (LineFamily.sum, ⟨8, by decide⟩)
+  have h16 := hline (LineFamily.difference, ⟨5, by decide⟩)
+  have h17 := hline (LineFamily.difference, ⟨3, by decide⟩)
+  have h18 := hline (LineFamily.difference, ⟨7, by decide⟩)
+  norm_num [p0Point, OnLine, lineValue, bitNat] at h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 ⊢
+  exact n6p0_sat (x 0) (x 1) (x 2) (x 3) (x 4) (x 5)
+    (x 6) (x 7) (x 8) (x 9) (x 10) (x 11)
+    (x 12) (x 13) (x 14) (x 15) (x 16) (x 17)
+    h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18
+
+private theorem p1_bridge
+    (x : Fin 18 → Bool)
+    (hline : ∀ line : PrincipalLine 6,
+      (Finset.univ.filter fun i => x i = true ∧ OnLine line (p1Point i)).card ≤ 2) :
+    (Finset.univ.filter fun i => x i = true).card ≤ 8 := by
+  have h0 := hline (LineFamily.row, ⟨0, by decide⟩)
+  have h1 := hline (LineFamily.row, ⟨1, by decide⟩)
+  have h2 := hline (LineFamily.row, ⟨2, by decide⟩)
+  have h3 := hline (LineFamily.row, ⟨3, by decide⟩)
+  have h4 := hline (LineFamily.row, ⟨4, by decide⟩)
+  have h5 := hline (LineFamily.row, ⟨5, by decide⟩)
+  have h6 := hline (LineFamily.column, ⟨1, by decide⟩)
+  have h7 := hline (LineFamily.column, ⟨3, by decide⟩)
+  have h8 := hline (LineFamily.column, ⟨5, by decide⟩)
+  have h9 := hline (LineFamily.column, ⟨0, by decide⟩)
+  have h10 := hline (LineFamily.column, ⟨2, by decide⟩)
+  have h11 := hline (LineFamily.column, ⟨4, by decide⟩)
+  have h12 := hline (LineFamily.sum, ⟨3, by decide⟩)
+  have h13 := hline (LineFamily.sum, ⟨5, by decide⟩)
+  have h14 := hline (LineFamily.sum, ⟨7, by decide⟩)
+  have h15 := hline (LineFamily.difference, ⟨4, by decide⟩)
+  have h16 := hline (LineFamily.difference, ⟨2, by decide⟩)
+  have h17 := hline (LineFamily.difference, ⟨6, by decide⟩)
+  have h18 := hline (LineFamily.difference, ⟨8, by decide⟩)
+  norm_num [p1Point, OnLine, lineValue, bitNat] at h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18 ⊢
+  exact n6p1_sat (x 0) (x 1) (x 2) (x 3) (x 4) (x 5)
+    (x 6) (x 7) (x 8) (x 9) (x 10) (x 11)
+    (x 12) (x 13) (x 14) (x 15) (x 16) (x 17)
+    h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18
+
+#print axioms p0_bridge
+#print axioms p1_bridge
+
+end Checkerboard
diff --git a/Checkerboard/N6Explicit.lean b/Checkerboard/N6Explicit.lean
new file mode 100644
index 00000000..0bcf2101
--- /dev/null
+++ b/Checkerboard/N6Explicit.lean
@@ -0,0 +1,322 @@
+import Checkerboard.FourCertificate
+import Checkerboard.N6SATTest
+
+/-!
+# Explicit 6×6 checkerboard base cases
+
+The quadratic relaxation is not integral on the 6-board.  This module transports
+an arbitrary monochromatic no-three-in-line set to eighteen Boolean indicators,
+uses closed certificates for the relevant row, column, and diagonal fibers, and
+then applies the compact Presburger certificates in `N6SATTest`.
+
+Proof developed by Dominic Dabish. ProofOrchestrator, using OpenAI GPT-5.6 Thinking,
+assisted with the mathematical argument, Lean formalization, and submission
+preparation. All formal claims are checked by the repository-pinned Lean compiler.
+-/
+
+namespace Checkerboard
+
+set_option maxHeartbeats 0
+set_option maxRecDepth 1000000
+
+private def n6p0Point : Fin 18 → Point 6 := ![
+  ((0 : Fin 6), (0 : Fin 6)), ((0 : Fin 6), (2 : Fin 6)),
+  ((0 : Fin 6), (4 : Fin 6)), ((1 : Fin 6), (1 : Fin 6)),
+  ((1 : Fin 6), (3 : Fin 6)), ((1 : Fin 6), (5 : Fin 6)),
+  ((2 : Fin 6), (0 : Fin 6)), ((2 : Fin 6), (2 : Fin 6)),
+  ((2 : Fin 6), (4 : Fin 6)), ((3 : Fin 6), (1 : Fin 6)),
+  ((3 : Fin 6), (3 : Fin 6)), ((3 : Fin 6), (5 : Fin 6)),
+  ((4 : Fin 6), (0 : Fin 6)), ((4 : Fin 6), (2 : Fin 6)),
+  ((4 : Fin 6), (4 : Fin 6)), ((5 : Fin 6), (1 : Fin 6)),
+  ((5 : Fin 6), (3 : Fin 6)), ((5 : Fin 6), (5 : Fin 6))]
+
+private def n6p1Point : Fin 18 → Point 6 := ![
+  ((0 : Fin 6), (1 : Fin 6)), ((0 : Fin 6), (3 : Fin 6)),
+  ((0 : Fin 6), (5 : Fin 6)), ((1 : Fin 6), (0 : Fin 6)),
+  ((1 : Fin 6), (2 : Fin 6)), ((1 : Fin 6), (4 : Fin 6)),
+  ((2 : Fin 6), (1 : Fin 6)), ((2 : Fin 6), (3 : Fin 6)),
+  ((2 : Fin 6), (5 : Fin 6)), ((3 : Fin 6), (0 : Fin 6)),
+  ((3 : Fin 6), (2 : Fin 6)), ((3 : Fin 6), (4 : Fin 6)),
+  ((4 : Fin 6), (1 : Fin 6)), ((4 : Fin 6), (3 : Fin 6)),
+  ((4 : Fin 6), (5 : Fin 6)), ((5 : Fin 6), (0 : Fin 6)),
+  ((5 : Fin 6), (2 : Fin 6)), ((5 : Fin 6), (4 : Fin 6))]
+
+private theorem n6p0_injective : Function.Injective n6p0Point := by decide
+private theorem n6p1_injective : Function.Injective n6p1Point := by decide
+
+private theorem n6p0_surjective :
+    ∀ p : Point 6, InColor 0 p → ∃ i, n6p0Point i = p := by
+  letI : DecidablePred (fun p : Point 6 =>
+      InColor 0 p → ∃ i, n6p0Point i = p) := by
+    intro p
+    unfold InColor
+    infer_instance
+  exact of_decide_eq_true rfl
+
+private theorem n6p1_surjective :
+    ∀ p : Point 6, InColor 1 p → ∃ i, n6p1Point i = p := by
+  letI : DecidablePred (fun p : Point 6 =>
+      InColor 1 p → ∃ i, n6p1Point i = p) := by
+    intro p
+    unfold InColor
+    infer_instance
+  exact of_decide_eq_true rfl
+
+private def chosenIndices (point : Fin 18 → Point 6)
+    (s : Finset (Point 6)) : Finset (Fin 18) :=
+  Finset.univ.filter fun i => point i ∈ s
+
+private def chosenOnLine (point : Fin 18 → Point 6)
+    (s : Finset (Point 6)) (line : PrincipalLine 6) : Finset (Fin 18) :=
+  Finset.univ.filter fun i => point i ∈ s ∧ OnLine line (point i)
+
+private theorem card_filter_bool {α : Type*} (s : Finset α) (x : α → Bool) :
+    (s.filter fun i => x i = true).card =
+      Finset.sum s (fun i => bitNat (x i)) := by
+  classical
+  induction s using Finset.induction_on with
+  | empty => simp
+  | @insert a s ha ih =>
+      cases hxa : x a <;> simp [ha, ih, hxa, bitNat]
+
+private theorem card_filter_bool_and {α : Type*} (s : Finset α)
+    (x : α → Bool) (p : α → Prop) [DecidablePred p] :
+    (s.filter fun i => x i = true ∧ p i).card =
+      Finset.sum (s.filter p) (fun i => bitNat (x i)) := by
+  classical
+  have hfilter :
+      s.filter (fun i => x i = true ∧ p i) =
+        (s.filter p).filter (fun i => x i = true) := by
+    ext i
+    simp [and_comm, and_left_comm, and_assoc]
+  rw [hfilter]
+  exact card_filter_bool (s.filter p) x
+
+private theorem chosenIndices_image
+    {parity : ℕ} (point : Fin 18 → Point 6)
+    (hsurj : ∀ p : Point 6, InColor parity p → ∃ i, point i = p)
+    (s : Finset (Point 6)) (hcolor : Monochromatic parity s) :
+    (chosenIndices point s).image point = s := by
+  ext p
+  constructor
+  · intro hp
+    rcases Finset.mem_image.mp hp with ⟨i, hi, rfl⟩
+    exact (Finset.mem_filter.mp hi).2
+  · intro hp
+    obtain ⟨i, hi⟩ := hsurj p (hcolor ⟨p, hp⟩)
+    subst p
+    apply Finset.mem_image.mpr
+    exact ⟨i, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hp⟩, rfl⟩
+
+private theorem chosenOnLine_image
+    {parity : ℕ} (point : Fin 18 → Point 6)
+    (hsurj : ∀ p : Point 6, InColor parity p → ∃ i, point i = p)
+    (s : Finset (Point 6)) (hcolor : Monochromatic parity s)
+    (line : PrincipalLine 6) :
+    (chosenOnLine point s line).image point = s.filter (OnLine line) := by
+  ext p
+  constructor
+  · intro hp
+    rcases Finset.mem_image.mp hp with ⟨i, hi, rfl⟩
+    exact Finset.mem_filter.mpr (Finset.mem_filter.mp hi).2
+  · intro hp
+    have hpS := (Finset.mem_filter.mp hp).1
+    have hpL := (Finset.mem_filter.mp hp).2
+    obtain ⟨i, hi⟩ := hsurj p (hcolor ⟨p, hpS⟩)
+    subst p
+    apply Finset.mem_image.mpr
+    exact ⟨i, Finset.mem_filter.mpr
+      ⟨Finset.mem_univ _, ⟨hpS, hpL⟩⟩, rfl⟩
+
+private theorem upper_of_boolean_certificate
+    {parity : ℕ} (point : Fin 18 → Point 6)
+    (hinj : Function.Injective point)
+    (hsurj : ∀ p : Point 6, InColor parity p → ∃ i, point i = p)
+    (hfinite : ∀ x : Fin 18 → Bool,
+      (∀ line : PrincipalLine 6,
+        (Finset.univ.filter fun i => x i = true ∧ OnLine line (point i)).card ≤ 2) →
+      (Finset.univ.filter fun i => x i = true).card ≤ 8)
+    (s : Finset (Point 6))
+    (hcolor : Monochromatic parity s) (hntil : NoThreeInLine s) :
+    s.card ≤ 8 := by
+  let x : Fin 18 → Bool := fun i => decide (point i ∈ s)
+  have hline : ∀ line : PrincipalLine 6,
+      (Finset.univ.filter fun i => x i = true ∧ OnLine line (point i)).card ≤ 2 := by
+    intro line
+    have himage := chosenOnLine_image point hsurj s hcolor line
+    have hcardImage := Finset.card_image_of_injective
+      (chosenOnLine point s line) hinj
+    have hchosen :
+        (chosenOnLine point s line).card = (s.filter (OnLine line)).card := by
+      calc
+        (chosenOnLine point s line).card =
+            ((chosenOnLine point s line).image point).card := hcardImage.symm
+        _ = (s.filter (OnLine line)).card := congrArg Finset.card himage
+    have heq :
+        (Finset.univ.filter fun i => x i = true ∧ OnLine line (point i)).card =
+          (s.filter (OnLine line)).card := by
+      simpa [x, chosenOnLine] using hchosen
+    rw [heq]
+    exact principalLine_card_le_two hntil line
+  have hbool := hfinite x hline
+  have himage := chosenIndices_image point hsurj s hcolor
+  have hcardImage := Finset.card_image_of_injective (chosenIndices point s) hinj
+  have hchosen : (chosenIndices point s).card = s.card := by
+    calc
+      (chosenIndices point s).card = ((chosenIndices point s).image point).card :=
+        hcardImage.symm
+      _ = s.card := congrArg Finset.card himage
+  have heq : (Finset.univ.filter fun i => x i = true).card = s.card := by
+    simpa [x, chosenIndices] using hchosen
+  rwa [heq] at hbool
+
+private def p0Line : Fin 19 → PrincipalLine 6 := ![
+  (.row, ⟨0, by decide⟩), (.row, ⟨1, by decide⟩),
+  (.row, ⟨2, by decide⟩), (.row, ⟨3, by decide⟩),
+  (.row, ⟨4, by decide⟩), (.row, ⟨5, by decide⟩),
+  (.column, ⟨0, by decide⟩), (.column, ⟨2, by decide⟩),
+  (.column, ⟨4, by decide⟩), (.column, ⟨1, by decide⟩),
+  (.column, ⟨3, by decide⟩), (.column, ⟨5, by decide⟩),
+  (.sum, ⟨2, by decide⟩), (.sum, ⟨4, by decide⟩),
+  (.sum, ⟨6, by decide⟩), (.sum, ⟨8, by decide⟩),
+  (.difference, ⟨5, by decide⟩), (.difference, ⟨3, by decide⟩),
+  (.difference, ⟨7, by decide⟩)]
+
+private def p0Index : Fin 19 → Finset (Fin 18) := ![
+  {0, 1, 2}, {3, 4, 5}, {6, 7, 8}, {9, 10, 11},
+  {12, 13, 14}, {15, 16, 17}, {0, 6, 12}, {1, 7, 13},
+  {2, 8, 14}, {3, 9, 15}, {4, 10, 16}, {5, 11, 17},
+  {1, 3, 6}, {2, 4, 7, 9, 12}, {5, 8, 10, 13, 15},
+  {11, 14, 16}, {0, 3, 7, 10, 14, 17}, {1, 4, 8, 11},
+  {6, 9, 13, 16}]
+
+private def p1Line : Fin 19 → PrincipalLine 6 := ![
+  (.row, ⟨0, by decide⟩), (.row, ⟨1, by decide⟩),
+  (.row, ⟨2, by decide⟩), (.row, ⟨3, by decide⟩),
+  (.row, ⟨4, by decide⟩), (.row, ⟨5, by decide⟩),
+  (.column, ⟨1, by decide⟩), (.column, ⟨3, by decide⟩),
+  (.column, ⟨5, by decide⟩), (.column, ⟨0, by decide⟩),
+  (.column, ⟨2, by decide⟩), (.column, ⟨4, by decide⟩),
+  (.sum, ⟨3, by decide⟩), (.sum, ⟨5, by decide⟩),
+  (.sum, ⟨7, by decide⟩), (.difference, ⟨4, by decide⟩),
+  (.difference, ⟨2, by decide⟩), (.difference, ⟨6, by decide⟩),
+  (.difference, ⟨8, by decide⟩)]
+
+private def p1Index : Fin 19 → Finset (Fin 18) := ![
+  {0, 1, 2}, {3, 4, 5}, {6, 7, 8}, {9, 10, 11},
+  {12, 13, 14}, {15, 16, 17}, {0, 6, 12}, {1, 7, 13},
+  {2, 8, 14}, {3, 9, 15}, {4, 10, 16}, {5, 11, 17},
+  {1, 4, 6, 9}, {2, 5, 7, 10, 12, 15}, {8, 11, 13, 16},
+  {0, 4, 7, 11, 14}, {1, 5, 8}, {3, 6, 10, 13, 17},
+  {9, 12, 16}]
+
+private theorem p0_line_indices (j : Fin 19) :
+    Finset.univ.filter (fun i => OnLine (p0Line j) (n6p0Point i)) = p0Index j := by
+  fin_cases j <;> decide
+
+private theorem p1_line_indices (j : Fin 19) :
+    Finset.univ.filter (fun i => OnLine (p1Line j) (n6p1Point i)) = p1Index j := by
+  fin_cases j <;> decide
+
+private theorem line_sum_le_two
+    (point : Fin 18 → Point 6) (x : Fin 18 → Bool)
+    (line : PrincipalLine 6) (idx : Finset (Fin 18))
+    (hidx : Finset.univ.filter (fun i => OnLine line (point i)) = idx)
+    (hline : (Finset.univ.filter fun i =>
+      x i = true ∧ OnLine line (point i)).card ≤ 2) :
+    Finset.sum idx (fun i => bitNat (x i)) ≤ 2 := by
+  rw [card_filter_bool_and, hidx] at hline
+  exact hline
+
+private def all18 : Finset (Fin 18) :=
+  {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17}
+
+private theorem all18_eq_univ : all18 = Finset.univ := by decide
+
+private theorem n6p0_boolean_bound :
+    ∀ x : Fin 18 → Bool,
+      (∀ line : PrincipalLine 6,
+        (Finset.univ.filter fun i =>
+          x i = true ∧ OnLine line (n6p0Point i)).card ≤ 2) →
+      (Finset.univ.filter fun i => x i = true).card ≤ 8 := by
+  intro x hline
+  have hb (j : Fin 19) : Finset.sum (p0Index j) (fun i => bitNat (x i)) ≤ 2 :=
+    line_sum_le_two n6p0Point x (p0Line j) (p0Index j)
+      (p0_line_indices j) (hline (p0Line j))
+  have h0 : bitNat (x 0) + bitNat (x 1) + bitNat (x 2) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 0
+  have h1 : bitNat (x 3) + bitNat (x 4) + bitNat (x 5) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 1
+  have h2 : bitNat (x 6) + bitNat (x 7) + bitNat (x 8) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 2
+  have h3 : bitNat (x 9) + bitNat (x 10) + bitNat (x 11) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 3
+  have h4 : bitNat (x 12) + bitNat (x 13) + bitNat (x 14) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 4
+  have h5 : bitNat (x 15) + bitNat (x 16) + bitNat (x 17) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 5
+  have h6 : bitNat (x 0) + bitNat (x 6) + bitNat (x 12) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 6
+  have h7 : bitNat (x 1) + bitNat (x 7) + bitNat (x 13) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 7
+  have h8 : bitNat (x 2) + bitNat (x 8) + bitNat (x 14) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 8
+  have h9 : bitNat (x 3) + bitNat (x 9) + bitNat (x 15) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 9
+  have h10 : bitNat (x 4) + bitNat (x 10) + bitNat (x 16) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 10
+  have h11 : bitNat (x 5) + bitNat (x 11) + bitNat (x 17) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 11
+  have h12 : bitNat (x 1) + bitNat (x 3) + bitNat (x 6) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 12
+  have h13 : bitNat (x 2) + bitNat (x 4) + bitNat (x 7) + bitNat (x 9) + bitNat (x 12) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 13
+  have h14 : bitNat (x 5) + bitNat (x 8) + bitNat (x 10) + bitNat (x 13) + bitNat (x 15) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 14
+  have h15 : bitNat (x 11) + bitNat (x 14) + bitNat (x 16) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 15
+  have h16 : bitNat (x 0) + bitNat (x 3) + bitNat (x 7) + bitNat (x 10) + bitNat (x 14) + bitNat (x 17) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 16
+  have h17 : bitNat (x 1) + bitNat (x 4) + bitNat (x 8) + bitNat (x 11) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 17
+  have h18 : bitNat (x 6) + bitNat (x 9) + bitNat (x 13) + bitNat (x 16) ≤ 2 := by simpa [p0Index, Nat.add_assoc] using hb 18
+  rw [card_filter_bool]
+  rw [← all18_eq_univ]
+  simpa [all18, Nat.add_assoc] using
+    n6p0_sat (x 0) (x 1) (x 2) (x 3) (x 4) (x 5)
+      (x 6) (x 7) (x 8) (x 9) (x 10) (x 11)
+      (x 12) (x 13) (x 14) (x 15) (x 16) (x 17)
+      h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18
+
+private theorem n6p1_boolean_bound :
+    ∀ x : Fin 18 → Bool,
+      (∀ line : PrincipalLine 6,
+        (Finset.univ.filter fun i =>
+          x i = true ∧ OnLine line (n6p1Point i)).card ≤ 2) →
+      (Finset.univ.filter fun i => x i = true).card ≤ 8 := by
+  intro x hline
+  have hb (j : Fin 19) : Finset.sum (p1Index j) (fun i => bitNat (x i)) ≤ 2 :=
+    line_sum_le_two n6p1Point x (p1Line j) (p1Index j)
+      (p1_line_indices j) (hline (p1Line j))
+  have h0 : bitNat (x 0) + bitNat (x 1) + bitNat (x 2) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 0
+  have h1 : bitNat (x 3) + bitNat (x 4) + bitNat (x 5) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 1
+  have h2 : bitNat (x 6) + bitNat (x 7) + bitNat (x 8) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 2
+  have h3 : bitNat (x 9) + bitNat (x 10) + bitNat (x 11) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 3
+  have h4 : bitNat (x 12) + bitNat (x 13) + bitNat (x 14) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 4
+  have h5 : bitNat (x 15) + bitNat (x 16) + bitNat (x 17) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 5
+  have h6 : bitNat (x 0) + bitNat (x 6) + bitNat (x 12) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 6
+  have h7 : bitNat (x 1) + bitNat (x 7) + bitNat (x 13) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 7
+  have h8 : bitNat (x 2) + bitNat (x 8) + bitNat (x 14) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 8
+  have h9 : bitNat (x 3) + bitNat (x 9) + bitNat (x 15) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 9
+  have h10 : bitNat (x 4) + bitNat (x 10) + bitNat (x 16) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 10
+  have h11 : bitNat (x 5) + bitNat (x 11) + bitNat (x 17) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 11
+  have h12 : bitNat (x 1) + bitNat (x 4) + bitNat (x 6) + bitNat (x 9) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 12
+  have h13 : bitNat (x 2) + bitNat (x 5) + bitNat (x 7) + bitNat (x 10) + bitNat (x 12) + bitNat (x 15) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 13
+  have h14 : bitNat (x 8) + bitNat (x 11) + bitNat (x 13) + bitNat (x 16) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 14
+  have h15 : bitNat (x 0) + bitNat (x 4) + bitNat (x 7) + bitNat (x 11) + bitNat (x 14) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 15
+  have h16 : bitNat (x 1) + bitNat (x 5) + bitNat (x 8) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 16
+  have h17 : bitNat (x 3) + bitNat (x 6) + bitNat (x 10) + bitNat (x 13) + bitNat (x 17) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 17
+  have h18 : bitNat (x 9) + bitNat (x 12) + bitNat (x 16) ≤ 2 := by simpa [p1Index, Nat.add_assoc] using hb 18
+  rw [card_filter_bool]
+  rw [← all18_eq_univ]
+  simpa [all18, Nat.add_assoc] using
+    n6p1_sat (x 0) (x 1) (x 2) (x 3) (x 4) (x 5)
+      (x 6) (x 7) (x 8) (x 9) (x 10) (x 11)
+      (x 12) (x 13) (x 14) (x 15) (x 16) (x 17)
+      h0 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13 h14 h15 h16 h17 h18
+
+/-- `D_mono(6,0) ≤ 8`. -/
+theorem n6_zero_upper (s : Finset (Point 6))
+    (hcolor : Monochromatic 0 s) (hntil : NoThreeInLine s) : s.card ≤ 8 := by
+  exact upper_of_boolean_certificate n6p0Point n6p0_injective n6p0_surjective
+    n6p0_boolean_bound s hcolor hntil
+
+/-- `D_mono(6,1) ≤ 8`. -/
+theorem n6_one_upper (s : Finset (Point 6))
+    (hcolor : Monochromatic 1 s) (hntil : NoThreeInLine s) : s.card ≤ 8 := by
+  exact upper_of_boolean_certificate n6p1Point n6p1_injective n6p1_surjective
+    n6p1_boolean_bound s hcolor hntil
+
+end Checkerboard
diff --git a/Checkerboard/N6SATTest.lean b/Checkerboard/N6SATTest.lean
new file mode 100644
index 00000000..fe71cf41
--- /dev/null
+++ b/Checkerboard/N6SATTest.lean
@@ -0,0 +1,153 @@
+import Mathlib
+
+/-!
+# Compact 6×6 checkerboard arithmetic certificates
+
+Proof developed by Dominic Dabish. ProofOrchestrator, using OpenAI GPT-5.6 Thinking,
+assisted with the mathematical argument, Lean formalization, and submission
+preparation. All formal claims are checked by the repository-pinned Lean compiler.
+-/
+
+namespace Checkerboard
+
+set_option maxHeartbeats 0
+
+/-- Convert a Boolean selection bit to its natural indicator. -/
+def bitNat (b : Bool) : ℕ := if b then 1 else 0
+
+@[simp] theorem bitNat_false : bitNat false = 0 := rfl
+@[simp] theorem bitNat_true : bitNat true = 1 := rfl
+
+theorem bitNat_le_one (b : Bool) : bitNat b ≤ 1 := by
+  cases b <;> simp
+
+/-- Integer certificate for the even checkerboard color class on the 6-board. -/
+theorem n6p0_sat
+    (x0 : Bool) (x1 : Bool) (x2 : Bool) (x3 : Bool) (x4 : Bool) (x5 : Bool)
+    (x6 : Bool) (x7 : Bool) (x8 : Bool) (x9 : Bool) (x10 : Bool) (x11 : Bool)
+    (x12 : Bool) (x13 : Bool) (x14 : Bool) (x15 : Bool) (x16 : Bool) (x17 : Bool)
+    (h0 : bitNat x0 + bitNat x1 + bitNat x2 ≤ 2)
+    (h1 : bitNat x3 + bitNat x4 + bitNat x5 ≤ 2)
+    (h2 : bitNat x6 + bitNat x7 + bitNat x8 ≤ 2)
+    (h3 : bitNat x9 + bitNat x10 + bitNat x11 ≤ 2)
+    (h4 : bitNat x12 + bitNat x13 + bitNat x14 ≤ 2)
+    (h5 : bitNat x15 + bitNat x16 + bitNat x17 ≤ 2)
+    (h6 : bitNat x0 + bitNat x6 + bitNat x12 ≤ 2)
+    (h7 : bitNat x1 + bitNat x7 + bitNat x13 ≤ 2)
+    (h8 : bitNat x2 + bitNat x8 + bitNat x14 ≤ 2)
+    (h9 : bitNat x3 + bitNat x9 + bitNat x15 ≤ 2)
+    (h10 : bitNat x4 + bitNat x10 + bitNat x16 ≤ 2)
+    (h11 : bitNat x5 + bitNat x11 + bitNat x17 ≤ 2)
+    (h12 : bitNat x1 + bitNat x3 + bitNat x6 ≤ 2)
+    (h13 : bitNat x2 + bitNat x4 + bitNat x7 + bitNat x9 + bitNat x12 ≤ 2)
+    (h14 : bitNat x5 + bitNat x8 + bitNat x10 + bitNat x13 + bitNat x15 ≤ 2)
+    (h15 : bitNat x11 + bitNat x14 + bitNat x16 ≤ 2)
+    (h16 : bitNat x0 + bitNat x3 + bitNat x7 + bitNat x10 + bitNat x14 + bitNat x17 ≤ 2)
+    (h17 : bitNat x1 + bitNat x4 + bitNat x8 + bitNat x11 ≤ 2)
+    (h18 : bitNat x6 + bitNat x9 + bitNat x13 + bitNat x16 ≤ 2) :
+    bitNat x0 + bitNat x1 + bitNat x2 + bitNat x3 + bitNat x4 + bitNat x5 +
+      bitNat x6 + bitNat x7 + bitNat x8 + bitNat x9 + bitNat x10 + bitNat x11 +
+      bitNat x12 + bitNat x13 + bitNat x14 + bitNat x15 + bitNat x16 + bitNat x17 ≤ 8 := by
+  have hx0 := bitNat_le_one x0
+  have hx1 := bitNat_le_one x1
+  have hx2 := bitNat_le_one x2
+  have hx3 := bitNat_le_one x3
+  have hx4 := bitNat_le_one x4
+  have hx5 := bitNat_le_one x5
+  have hx6 := bitNat_le_one x6
+  have hx7 := bitNat_le_one x7
+  have hx8 := bitNat_le_one x8
+  have hx9 := bitNat_le_one x9
+  have hx10 := bitNat_le_one x10
+  have hx11 := bitNat_le_one x11
+  have hx12 := bitNat_le_one x12
+  have hx13 := bitNat_le_one x13
+  have hx14 := bitNat_le_one x14
+  have hx15 := bitNat_le_one x15
+  have hx16 := bitNat_le_one x16
+  have hx17 := bitNat_le_one x17
+  cases x0 <;> cases x1
+  · simp only [bitNat_false, bitNat_true, Nat.zero_add, Nat.add_zero] at *
+    clear h0 h1 h2 h3 h4 h6 h7 h9 h10 h12
+      hx0 hx1 hx2 hx4 hx5 hx7 hx8 hx9 hx10 hx13 hx14 hx15 hx16 hx17
+    omega
+  · simp only [bitNat_false, bitNat_true, Nat.zero_add, Nat.add_zero] at *
+    clear h0 h1 h2 h3 h6 h7 h9 h10
+      hx0 hx1 hx2 hx3 hx4 hx5 hx7 hx8 hx9 hx10 hx11 hx12 hx13 hx14 hx15 hx16 hx17
+    omega
+  · simp only [bitNat_false, bitNat_true, Nat.zero_add, Nat.add_zero] at *
+    clear h0 h2 h3 h4 h7 h8 h9 h10 h11 h12
+      hx0 hx1 hx3 hx4 hx5 hx6 hx7 hx8 hx9 hx10 hx12 hx13 hx14 hx15 hx16 hx17
+    omega
+  · simp only [bitNat_false, bitNat_true, Nat.zero_add, Nat.add_zero] at *
+    clear h1 h2 h3 h4 h7 h8 h10 h12
+      hx0 hx1 hx2 hx3 hx4 hx6 hx7 hx8 hx9 hx10 hx11 hx12 hx13 hx14 hx15 hx17
+    omega
+
+/-- Integer certificate for the odd checkerboard color class on the 6-board. -/
+theorem n6p1_sat
+    (x0 : Bool) (x1 : Bool) (x2 : Bool) (x3 : Bool) (x4 : Bool) (x5 : Bool)
+    (x6 : Bool) (x7 : Bool) (x8 : Bool) (x9 : Bool) (x10 : Bool) (x11 : Bool)
+    (x12 : Bool) (x13 : Bool) (x14 : Bool) (x15 : Bool) (x16 : Bool) (x17 : Bool)
+    (h0 : bitNat x0 + bitNat x1 + bitNat x2 ≤ 2)
+    (h1 : bitNat x3 + bitNat x4 + bitNat x5 ≤ 2)
+    (h2 : bitNat x6 + bitNat x7 + bitNat x8 ≤ 2)
+    (h3 : bitNat x9 + bitNat x10 + bitNat x11 ≤ 2)
+    (h4 : bitNat x12 + bitNat x13 + bitNat x14 ≤ 2)
+    (h5 : bitNat x15 + bitNat x16 + bitNat x17 ≤ 2)
+    (h6 : bitNat x0 + bitNat x6 + bitNat x12 ≤ 2)
+    (h7 : bitNat x1 + bitNat x7 + bitNat x13 ≤ 2)
+    (h8 : bitNat x2 + bitNat x8 + bitNat x14 ≤ 2)
+    (h9 : bitNat x3 + bitNat x9 + bitNat x15 ≤ 2)
+    (h10 : bitNat x4 + bitNat x10 + bitNat x16 ≤ 2)
+    (h11 : bitNat x5 + bitNat x11 + bitNat x17 ≤ 2)
+    (h12 : bitNat x1 + bitNat x4 + bitNat x6 + bitNat x9 ≤ 2)
+    (h13 : bitNat x2 + bitNat x5 + bitNat x7 + bitNat x10 + bitNat x12 + bitNat x15 ≤ 2)
+    (h14 : bitNat x8 + bitNat x11 + bitNat x13 + bitNat x16 ≤ 2)
+    (h15 : bitNat x0 + bitNat x4 + bitNat x7 + bitNat x11 + bitNat x14 ≤ 2)
+    (h16 : bitNat x1 + bitNat x5 + bitNat x8 ≤ 2)
+    (h17 : bitNat x3 + bitNat x6 + bitNat x10 + bitNat x13 + bitNat x17 ≤ 2)
+    (h18 : bitNat x9 + bitNat x12 + bitNat x16 ≤ 2) :
+    bitNat x0 + bitNat x1 + bitNat x2 + bitNat x3 + bitNat x4 + bitNat x5 +
+      bitNat x6 + bitNat x7 + bitNat x8 + bitNat x9 + bitNat x10 + bitNat x11 +
+      bitNat x12 + bitNat x13 + bitNat x14 + bitNat x15 + bitNat x16 + bitNat x17 ≤ 8 := by
+  have hx0 := bitNat_le_one x0
+  have hx1 := bitNat_le_one x1
+  have hx2 := bitNat_le_one x2
+  have hx3 := bitNat_le_one x3
+  have hx4 := bitNat_le_one x4
+  have hx5 := bitNat_le_one x5
+  have hx6 := bitNat_le_one x6
+  have hx7 := bitNat_le_one x7
+  have hx8 := bitNat_le_one x8
+  have hx9 := bitNat_le_one x9
+  have hx10 := bitNat_le_one x10
+  have hx11 := bitNat_le_one x11
+  have hx12 := bitNat_le_one x12
+  have hx13 := bitNat_le_one x13
+  have hx14 := bitNat_le_one x14
+  have hx15 := bitNat_le_one x15
+  have hx16 := bitNat_le_one x16
+  have hx17 := bitNat_le_one x17
+  cases x0 <;> cases x1
+  · simp only [bitNat_false, bitNat_true, Nat.zero_add, Nat.add_zero] at *
+    clear h0 h2 h3 h4 h6 h7 h10 h16
+      hx0 hx1 hx2 hx3 hx4 hx5 hx6 hx7 hx9 hx10 hx11 hx12 hx13 hx15 hx16 hx17
+    omega
+  · simp only [bitNat_false, bitNat_true, Nat.zero_add, Nat.add_zero] at *
+    clear h0 h1 h2 h3 h4 h6 h7 h10
+      hx0 hx1 hx2 hx4 hx5 hx6 hx7 hx8 hx9 hx10 hx11 hx12 hx13 hx15 hx16 hx17
+    omega
+  · simp only [bitNat_false, bitNat_true, Nat.zero_add, Nat.add_zero] at *
+    clear h0 h2 h3 h4 h6 h7 h10 h11 h16
+      hx0 hx1 hx2 hx3 hx4 hx6 hx7 hx10 hx11 hx12 hx13 hx14 hx15 hx16 hx17
+    omega
+  · simp only [bitNat_false, bitNat_true, Nat.zero_add, Nat.add_zero] at *
+    clear h1 h2 h3 h7 h8 h10 h11
+      hx0 hx1 hx2 hx3 hx4 hx5 hx6 hx7 hx9 hx10 hx11 hx12 hx13 hx14 hx15 hx16 hx17
+    omega
+
+#print axioms n6p0_sat
+#print axioms n6p1_sat
+
+end Checkerboard
diff --git a/Checkerboard/PolynomialSums.lean b/Checkerboard/PolynomialSums.lean
new file mode 100644
index 00000000..42f25401
--- /dev/null
+++ b/Checkerboard/PolynomialSums.lean
@@ -0,0 +1,138 @@
+import Mathlib
+
+namespace Checkerboard
+
+open scoped BigOperators
+
+theorem sum_range_affine_sq (n : ℕ) (a b : ℚ) :
+    (∑ i ∈ Finset.range n, (a * (i : ℚ) + b) ^ 2) =
+      a ^ 2 * ((n : ℚ) * ((n : ℚ) - 1) * (2 * (n : ℚ) - 1) / 6) +
+      2 * a * b * ((n : ℚ) * ((n : ℚ) - 1) / 2) +
+      (n : ℚ) * b ^ 2 := by
+  induction n with
+  | zero => norm_num
+  | succ n ih =>
+      rw [Finset.sum_range_succ, ih]
+      push_cast
+      ring
+
+theorem sum_range_quadratic_cap (N : ℕ) :
+    (∑ j ∈ Finset.range (2 * N + 1),
+      2 * ((N : ℚ) ^ 2 - ((j : ℚ) - N) ^ 2)) =
+      2 * (N : ℚ) * (2 * (N : ℚ) - 1) * (2 * (N : ℚ) + 1) / 3 := by
+  have h := sum_range_affine_sq (2 * N + 1) (1 : ℚ) (-(N : ℚ))
+  push_cast at h
+  have hsum :
+      (∑ j ∈ Finset.range (2 * N + 1), ((j : ℚ) - N) ^ 2) =
+        ∑ j ∈ Finset.range (2 * N + 1),
+          ((1 : ℚ) * (j : ℚ) + (-(N : ℚ))) ^ 2 := by
+    apply Finset.sum_congr rfl
+    intro j _
+    ring
+  calc
+    (∑ j ∈ Finset.range (2 * N + 1),
+      2 * ((N : ℚ) ^ 2 - ((j : ℚ) - N) ^ 2)) =
+        2 * (∑ j ∈ Finset.range (2 * N + 1),
+          ((N : ℚ) ^ 2 - ((j : ℚ) - N) ^ 2)) := by
+          rw [Finset.mul_sum]
+    _ = 2 * ((2 * (N : ℚ) + 1) * (N : ℚ) ^ 2 -
+          ∑ j ∈ Finset.range (2 * N + 1), ((j : ℚ) - N) ^ 2) := by
+          rw [Finset.sum_sub_distrib]
+          simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
+          push_cast
+          ring
+    _ = 2 * (N : ℚ) * (2 * (N : ℚ) - 1) *
+          (2 * (N : ℚ) + 1) / 3 := by
+          rw [hsum, h]
+          ring
+
+theorem sum_range_even_terms (k : ℕ) (f : ℕ → ℚ) :
+    (∑ j ∈ Finset.range (2 * k), if j % 2 = 0 then f j else 0) =
+      ∑ r ∈ Finset.range k, f (2 * r) := by
+  induction k with
+  | zero => simp
+  | succ k ih =>
+      simp only [Nat.mul_succ, Finset.sum_range_succ]
+      rw [ih]
+      norm_num [Nat.add_mod, Nat.mul_mod]
+
+theorem sum_range_odd_terms (k : ℕ) (f : ℕ → ℚ) :
+    (∑ j ∈ Finset.range (2 * k), if j % 2 = 1 then f j else 0) =
+      ∑ r ∈ Finset.range k, f (2 * r + 1) := by
+  induction k with
+  | zero => simp
+  | succ k ih =>
+      simp only [Nat.mul_succ, Finset.sum_range_succ]
+      rw [ih]
+      norm_num [Nat.add_mod, Nat.mul_mod]
+
+theorem sum_range_even_terms_succ (k : ℕ) (f : ℕ → ℚ) :
+    (∑ j ∈ Finset.range (2 * k + 1), if j % 2 = 0 then f j else 0) =
+      ∑ r ∈ Finset.range (k + 1), f (2 * r) := by
+  rw [Finset.sum_range_succ, sum_range_even_terms, Finset.sum_range_succ]
+  norm_num [Nat.add_mod, Nat.mul_mod]
+
+theorem sum_range_odd_terms_succ (k : ℕ) (f : ℕ → ℚ) :
+    (∑ j ∈ Finset.range (2 * k + 1), if j % 2 = 1 then f j else 0) =
+      ∑ r ∈ Finset.range k, f (2 * r + 1) := by
+  rw [Finset.sum_range_succ, sum_range_odd_terms]
+  norm_num [Nat.add_mod, Nat.mul_mod]
+
+theorem even_quadratic_cap_sum (m : ℕ) :
+    (∑ j ∈ Finset.range (4 * m + 1),
+      if j % 2 = 0 then
+        2 * ((2 * m : ℚ) ^ 2 - ((j : ℚ) - 2 * m) ^ 2)
+      else 0) =
+      8 * (m : ℚ) * (2 * (m : ℚ) - 1) *
+        (2 * (m : ℚ) + 1) / 3 := by
+  have h := sum_range_quadratic_cap m
+  rw [show 4 * m + 1 = 2 * (2 * m) + 1 by omega,
+    sum_range_even_terms_succ]
+  push_cast
+  calc
+    (∑ r ∈ Finset.range (2 * m + 1),
+      2 * ((2 * (m : ℚ)) ^ 2 -
+        (2 * (r : ℚ) - 2 * (m : ℚ)) ^ 2)) =
+        4 * (∑ r ∈ Finset.range (2 * m + 1),
+          2 * ((m : ℚ) ^ 2 - ((r : ℚ) - m) ^ 2)) := by
+          rw [Finset.mul_sum]
+          apply Finset.sum_congr rfl
+          intro r _
+          ring
+    _ = 8 * (m : ℚ) * (2 * (m : ℚ) - 1) *
+          (2 * (m : ℚ) + 1) / 3 := by
+          rw [h]
+          ring
+
+theorem odd_quadratic_cap_sum (m : ℕ) :
+    (∑ j ∈ Finset.range (4 * m + 1),
+      if j % 2 = 1 then
+        2 * ((2 * m : ℚ) ^ 2 - ((j : ℚ) - 2 * m) ^ 2)
+      else 0) =
+      4 * (m : ℚ) * (8 * (m : ℚ) ^ 2 + 1) / 3 := by
+  rw [show 4 * m + 1 = 2 * (2 * m) + 1 by omega,
+    sum_range_odd_terms_succ]
+  have h := sum_range_affine_sq (2 * m) (2 : ℚ)
+    (1 - 2 * (m : ℚ))
+  push_cast at h
+  simp_rw [Nat.cast_add, Nat.cast_mul, Nat.cast_one]
+  calc
+    (∑ r ∈ Finset.range (2 * m),
+      2 * ((2 * (m : ℚ)) ^ 2 -
+        (2 * (r : ℚ) + 1 - 2 * (m : ℚ)) ^ 2)) =
+        2 * (∑ r ∈ Finset.range (2 * m),
+          ((2 * (m : ℚ)) ^ 2 -
+            (2 * (r : ℚ) + 1 - 2 * (m : ℚ)) ^ 2)) := by
+          rw [Finset.mul_sum]
+    _ = 2 * ((2 * (m : ℚ)) * (2 * (m : ℚ)) ^ 2 -
+          ∑ r ∈ Finset.range (2 * m),
+            (2 * (r : ℚ) + (1 - 2 * (m : ℚ))) ^ 2) := by
+          rw [Finset.sum_sub_distrib]
+          simp only [Finset.sum_const, Finset.card_range, nsmul_eq_mul]
+          push_cast
+          ring
+    _ = 4 * (m : ℚ) * (8 * (m : ℚ) ^ 2 + 1) / 3 := by
+      rw [h]
+      ring
+
+end Checkerboard
diff --git a/Checkerboard/QuadraticCosts.lean b/Checkerboard/QuadraticCosts.lean
new file mode 100644
index 00000000..a9f3a0e5
--- /dev/null
+++ b/Checkerboard/QuadraticCosts.lean
@@ -0,0 +1,194 @@
+import Checkerboard.QuadraticWeights
+import Checkerboard.FinPolynomialSums
+
+/-!
+# Exact objectives of the quadratic line covers
+-/
+
+namespace Checkerboard
+
+open scoped BigOperators
+
+private def oddCapExpr (m : ℕ) {k : ℕ} (j : Fin k) : ℚ :=
+  2 * ((2 * m : ℚ) ^ 2 - ((j.1 : ℚ) - 2 * m) ^ 2)
+
+private def evenCapExpr (m : ℕ) {k : ℕ} (j : Fin k) : ℚ :=
+  2 * (((2 * m : ℚ) - 1) ^ 2 -
+    ((j.1 : ℚ) - ((2 * m : ℚ) - 1)) ^ 2)
+
+private theorem odd_axis_sum (m : ℕ) :
+    (∑ i : Fin (2 * m + 1), (2 * (i.1 : ℚ) - 2 * m) ^ 2) =
+      4 * (m : ℚ) * ((m : ℚ) + 1) * (2 * (m : ℚ) + 1) / 3 := by
+  have h := axis_quadratic_sum (2 * m + 1)
+  push_cast at h
+  calc
+    (∑ i : Fin (2 * m + 1), (2 * (i.1 : ℚ) - 2 * m) ^ 2) =
+        ∑ i : Fin (2 * m + 1),
+          (2 * (i.1 : ℚ) - (2 * (m : ℚ) + 1 - 1)) ^ 2 := by
+            apply Finset.sum_congr rfl
+            intro i _
+            ring
+    _ = (2 * (m : ℚ) + 1) * ((2 * (m : ℚ) + 1) ^ 2 - 1) / 3 := h
+    _ = 4 * (m : ℚ) * ((m : ℚ) + 1) * (2 * (m : ℚ) + 1) / 3 := by ring
+
+private theorem even_axis_sum (m : ℕ) :
+    (∑ i : Fin (2 * m),
+      (2 * (i.1 : ℚ) - ((2 * m : ℚ) - 1)) ^ 2) =
+      2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 := by
+  have h := axis_quadratic_sum (2 * m)
+  push_cast at h
+  calc
+    (∑ i : Fin (2 * m),
+      (2 * (i.1 : ℚ) - ((2 * m : ℚ) - 1)) ^ 2) =
+        (2 * (m : ℚ)) * ((2 * (m : ℚ)) ^ 2 - 1) / 3 := by
+          simpa using h
+    _ = 2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 := by ring
+
+private theorem odd_even_diag_sum (m : ℕ) :
+    (∑ j : Fin (2 * (2 * m + 1) - 1),
+      if j.1 % 2 = 0 then oddCapExpr m j else 0) =
+      8 * (m : ℚ) * (2 * (m : ℚ) - 1) *
+        (2 * (m : ℚ) + 1) / 3 := by
+  have hdim : 2 * (2 * m + 1) - 1 = 4 * m + 1 := by omega
+  rw [hdim]
+  simpa [oddCapExpr] using fin_even_quadratic_cap_sum m
+
+private theorem odd_odd_diag_sum (m : ℕ) :
+    (∑ j : Fin (2 * (2 * m + 1) - 1),
+      if j.1 % 2 = 1 then oddCapExpr m j else 0) =
+      4 * (m : ℚ) * (8 * (m : ℚ) ^ 2 + 1) / 3 := by
+  have hdim : 2 * (2 * m + 1) - 1 = 4 * m + 1 := by omega
+  rw [hdim]
+  simpa [oddCapExpr] using fin_odd_quadratic_cap_sum m
+
+private theorem parity_partition {k : ℕ} (f : Fin k → ℚ) :
+    (∑ j : Fin k, if j.1 % 2 = 0 then f j else 0) +
+        (∑ j : Fin k, if j.1 % 2 = 1 then f j else 0) =
+      ∑ j : Fin k, f j := by
+  rw [← Finset.sum_add_distrib]
+  apply Finset.sum_congr rfl
+  intro j _
+  rcases Nat.mod_two_eq_zero_or_one j.1 with h | h <;> simp [h]
+
+private theorem even_all_diag_sum (m : ℕ) (hm : 1 ≤ m) :
+    (∑ j : Fin (2 * (2 * m) - 1), evenCapExpr m j) =
+      2 * ((2 * m : ℚ) - 1) * (4 * (m : ℚ) - 3) *
+        (4 * (m : ℚ) - 1) / 3 := by
+  have hdim : 2 * (2 * m) - 1 = 2 * (2 * m - 1) + 1 := by omega
+  rw [hdim]
+  have h := fin_quadratic_cap_sum (2 * m - 1)
+  have htwo : 1 ≤ 2 * m := by omega
+  have hcast : (((2 * m - 1 : ℕ) : ℚ)) = 2 * (m : ℚ) - 1 := by
+    rw [Nat.cast_sub htwo]
+    norm_num
+  rw [hcast] at h
+  change (∑ j : Fin (2 * (2 * m - 1) + 1),
+    2 * ((2 * (m : ℚ) - 1) ^ 2 -
+      ((j.1 : ℚ) - (2 * (m : ℚ) - 1)) ^ 2)) = _
+  calc
+    _ = 2 * (2 * (m : ℚ) - 1) *
+        (2 * (2 * (m : ℚ) - 1) - 1) *
+        (2 * (2 * (m : ℚ) - 1) + 1) / 3 := h
+    _ = 2 * ((2 * m : ℚ) - 1) * (4 * (m : ℚ) - 3) *
+        (4 * (m : ℚ) - 1) / 3 := by ring
+
+/-- Exact objective for the fat color of an odd board. -/
+theorem oddQuadratic_cost_zero (m : ℕ) :
+    fourCost (oddQuadraticWeights m 0) =
+      16 * (m : ℚ) * (10 * (m : ℚ) ^ 2 + 3 * (m : ℚ) - 1) / 3 := by
+  change 2 * (
+    (∑ i : Fin (2 * m + 1), (2 * (i.1 : ℚ) - 2 * m) ^ 2) +
+    (∑ i : Fin (2 * m + 1), (2 * (i.1 : ℚ) - 2 * m) ^ 2) +
+    (∑ j : Fin (2 * (2 * m + 1) - 1),
+      if j.1 % 2 = 0 then oddCapExpr m j else 0) +
+    (∑ j : Fin (2 * (2 * m + 1) - 1),
+      if j.1 % 2 = 0 then oddCapExpr m j else 0)) = _
+  rw [odd_axis_sum, odd_even_diag_sum]
+  ring
+
+/-- Exact objective for the thin color of an odd board. -/
+theorem oddQuadratic_cost_one (m : ℕ) :
+    fourCost (oddQuadraticWeights m 1) =
+      16 * (m : ℚ) * (10 * (m : ℚ) ^ 2 + 3 * (m : ℚ) + 2) / 3 := by
+  change 2 * (
+    (∑ i : Fin (2 * m + 1), (2 * (i.1 : ℚ) - 2 * m) ^ 2) +
+    (∑ i : Fin (2 * m + 1), (2 * (i.1 : ℚ) - 2 * m) ^ 2) +
+    (∑ j : Fin (2 * (2 * m + 1) - 1),
+      if j.1 % 2 = 1 then oddCapExpr m j else 0) +
+    (∑ j : Fin (2 * (2 * m + 1) - 1),
+      if j.1 % 2 = 1 then oddCapExpr m j else 0)) = _
+  rw [odd_axis_sum, odd_odd_diag_sum]
+  ring
+
+/-- Both checkerboard colors have the same objective on an even board. -/
+theorem evenQuadratic_cost_zero (m : ℕ) (hm : 1 ≤ m) :
+    fourCost (evenQuadraticWeights m 0) =
+      4 * ((2 * m : ℚ) - 1) *
+        (20 * (m : ℚ) ^ 2 - 14 * (m : ℚ) + 3) / 3 := by
+  change 2 * (
+    (∑ i : Fin (2 * m),
+      (2 * (i.1 : ℚ) - ((2 * m : ℚ) - 1)) ^ 2) +
+    (∑ i : Fin (2 * m),
+      (2 * (i.1 : ℚ) - ((2 * m : ℚ) - 1)) ^ 2) +
+    (∑ j : Fin (2 * (2 * m) - 1),
+      if j.1 % 2 = 0 then evenCapExpr m j else 0) +
+    (∑ j : Fin (2 * (2 * m) - 1),
+      if j.1 % 2 = 1 then evenCapExpr m j else 0)) = _
+  rw [even_axis_sum]
+  have hpartition :=
+    parity_partition (fun j : Fin (2 * (2 * m) - 1) => evenCapExpr m j)
+  calc
+    2 * ((2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 +
+        2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 +
+        (∑ j : Fin (2 * (2 * m) - 1),
+          if j.1 % 2 = 0 then evenCapExpr m j else 0)) +
+        (∑ j : Fin (2 * (2 * m) - 1),
+          if j.1 % 2 = 1 then evenCapExpr m j else 0)) =
+      2 * (2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 +
+        2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 +
+        ((∑ j : Fin (2 * (2 * m) - 1),
+          if j.1 % 2 = 0 then evenCapExpr m j else 0) +
+        (∑ j : Fin (2 * (2 * m) - 1),
+          if j.1 % 2 = 1 then evenCapExpr m j else 0))) := by ring
+    _ = 2 * (2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 +
+        2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 +
+        (∑ j : Fin (2 * (2 * m) - 1), evenCapExpr m j)) := by rw [hpartition]
+    _ = _ := by rw [even_all_diag_sum m hm]; ring
+
+/-- Same objective for the other color of an even board. -/
+theorem evenQuadratic_cost_one (m : ℕ) (hm : 1 ≤ m) :
+    fourCost (evenQuadraticWeights m 1) =
+      4 * ((2 * m : ℚ) - 1) *
+        (20 * (m : ℚ) ^ 2 - 14 * (m : ℚ) + 3) / 3 := by
+  change 2 * (
+    (∑ i : Fin (2 * m),
+      (2 * (i.1 : ℚ) - ((2 * m : ℚ) - 1)) ^ 2) +
+    (∑ i : Fin (2 * m),
+      (2 * (i.1 : ℚ) - ((2 * m : ℚ) - 1)) ^ 2) +
+    (∑ j : Fin (2 * (2 * m) - 1),
+      if j.1 % 2 = 1 then evenCapExpr m j else 0) +
+    (∑ j : Fin (2 * (2 * m) - 1),
+      if j.1 % 2 = 0 then evenCapExpr m j else 0)) = _
+  rw [even_axis_sum]
+  have hpartition :=
+    parity_partition (fun j : Fin (2 * (2 * m) - 1) => evenCapExpr m j)
+  rw [add_comm] at hpartition
+  calc
+    2 * ((2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 +
+        2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 +
+        (∑ j : Fin (2 * (2 * m) - 1),
+          if j.1 % 2 = 1 then evenCapExpr m j else 0)) +
+        (∑ j : Fin (2 * (2 * m) - 1),
+          if j.1 % 2 = 0 then evenCapExpr m j else 0)) =
+      2 * (2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 +
+        2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 +
+        ((∑ j : Fin (2 * (2 * m) - 1),
+          if j.1 % 2 = 1 then evenCapExpr m j else 0) +
+        (∑ j : Fin (2 * (2 * m) - 1),
+          if j.1 % 2 = 0 then evenCapExpr m j else 0))) := by ring
+    _ = 2 * (2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 +
+        2 * (m : ℚ) * (4 * (m : ℚ) ^ 2 - 1) / 3 +
+        (∑ j : Fin (2 * (2 * m) - 1), evenCapExpr m j)) := by rw [hpartition]
+    _ = _ := by rw [even_all_diag_sum m hm]; ring
+
+end Checkerboard
diff --git a/Checkerboard/QuadraticWeights.lean b/Checkerboard/QuadraticWeights.lean
new file mode 100644
index 00000000..ebe25e1e
--- /dev/null
+++ b/Checkerboard/QuadraticWeights.lean
@@ -0,0 +1,151 @@
+import Checkerboard.FourCertificate
+
+/-!
+# Quadratic line-cover weights
+
+For a point `(x,y)` on an `n` board, put `N=n-1`, `u=x+y-N`,
+and `v=x-y`.  The exact identity
+
+`(2x-N)^2 + (2y-N)^2 + 2(N^2-u^2) + 2(N^2-v^2) = 4N^2`
+
+gives constant point coverage after retaining the diagonals of the required
+checkerboard parity.
+-/
+
+namespace Checkerboard
+
+private def oddCap (m : ℕ) {k : ℕ} (j : Fin k) : ℚ :=
+  2 * ((2 * m : ℚ) ^ 2 - ((j.1 : ℚ) - 2 * m) ^ 2)
+
+private def evenCap (m : ℕ) {k : ℕ} (j : Fin k) : ℚ :=
+  2 * (((2 * m : ℚ) - 1) ^ 2 -
+    ((j.1 : ℚ) - ((2 * m : ℚ) - 1)) ^ 2)
+
+/-- Quadratic cover for the odd board `n=2m+1`. -/
+def oddQuadraticWeights (m parity : ℕ) : FourWeights (2 * m + 1) where
+  row i := (2 * (i.1 : ℚ) - 2 * m) ^ 2
+  column i := (2 * (i.1 : ℚ) - 2 * m) ^ 2
+  sum j := if j.1 % 2 = parity % 2 then oddCap m j else 0
+  difference j := if j.1 % 2 = parity % 2 then oddCap m j else 0
+
+/-- Quadratic cover for the even board `n=2m`.  Difference-line indices are
+shifted by the odd number `2m-1`, hence use the opposite index parity. -/
+def evenQuadraticWeights (m parity : ℕ) : FourWeights (2 * m) where
+  row i := (2 * (i.1 : ℚ) - ((2 * m : ℚ) - 1)) ^ 2
+  column i := (2 * (i.1 : ℚ) - ((2 * m : ℚ) - 1)) ^ 2
+  sum j := if j.1 % 2 = parity % 2 then evenCap m j else 0
+  difference j :=
+    if j.1 % 2 = (parity + 1) % 2 then evenCap m j else 0
+
+private theorem oddCap_nonneg (m : ℕ)
+    (j : Fin (2 * (2 * m + 1) - 1)) : 0 ≤ oddCap m j := by
+  have hj0 : (0 : ℚ) ≤ j.1 := by positivity
+  have hjmax : (j.1 : ℚ) ≤ 4 * (m : ℚ) := by
+    exact_mod_cast (show j.1 ≤ 4 * m by omega)
+  have hprod : 0 ≤ (j.1 : ℚ) * (4 * (m : ℚ) - j.1) :=
+    mul_nonneg hj0 (sub_nonneg.mpr hjmax)
+  unfold oddCap
+  nlinarith
+
+private theorem evenCap_nonneg (m : ℕ) (hm : 1 ≤ m)
+    (j : Fin (2 * (2 * m) - 1)) : 0 ≤ evenCap m j := by
+  have hj0 : (0 : ℚ) ≤ j.1 := by positivity
+  have hjmax : (j.1 : ℚ) ≤ 2 * ((2 * m : ℚ) - 1) := by
+    have hjmaxNat : j.1 ≤ 2 * (2 * m - 1) := by omega
+    have htwo : 1 ≤ 2 * m := by omega
+    calc
+      (j.1 : ℚ) ≤ ((2 * (2 * m - 1) : ℕ) : ℚ) := by
+        exact_mod_cast hjmaxNat
+      _ = 2 * ((2 * m : ℚ) - 1) := by
+        norm_num [Nat.cast_sub htwo]
+  have hprod : 0 ≤ (j.1 : ℚ) *
+      (2 * ((2 * m : ℚ) - 1) - j.1) :=
+    mul_nonneg hj0 (sub_nonneg.mpr hjmax)
+  unfold evenCap
+  nlinarith
+
+/-- All four odd-board line weights are nonnegative. -/
+theorem oddQuadratic_nonnegative (m parity : ℕ) :
+    (∀ i, 0 ≤ (oddQuadraticWeights m parity).row i) ∧
+    (∀ i, 0 ≤ (oddQuadraticWeights m parity).column i) ∧
+    (∀ i, 0 ≤ (oddQuadraticWeights m parity).sum i) ∧
+    ∀ i, 0 ≤ (oddQuadraticWeights m parity).difference i := by
+  constructor
+  · intro i
+    simp [oddQuadraticWeights]
+    positivity
+  constructor
+  · intro i
+    simp [oddQuadraticWeights]
+    positivity
+  constructor
+  · intro i
+    simp only [oddQuadraticWeights]
+    split <;> simp_all [oddCap_nonneg]
+  · intro i
+    simp only [oddQuadraticWeights]
+    split <;> simp_all [oddCap_nonneg]
+
+/-- All four even-board line weights are nonnegative. -/
+theorem evenQuadratic_nonnegative (m parity : ℕ) (hm : 1 ≤ m) :
+    (∀ i, 0 ≤ (evenQuadraticWeights m parity).row i) ∧
+    (∀ i, 0 ≤ (evenQuadraticWeights m parity).column i) ∧
+    (∀ i, 0 ≤ (evenQuadraticWeights m parity).sum i) ∧
+    ∀ i, 0 ≤ (evenQuadraticWeights m parity).difference i := by
+  constructor
+  · intro i
+    simp [evenQuadraticWeights]
+    positivity
+  constructor
+  · intro i
+    simp [evenQuadraticWeights]
+    positivity
+  constructor
+  · intro i
+    simp only [evenQuadraticWeights]
+    split <;> simp_all [evenCap_nonneg m hm]
+  · intro i
+    simp only [evenQuadraticWeights]
+    split <;> simp_all [evenCap_nonneg m hm]
+
+/-- Constant coverage on an odd board. -/
+theorem oddQuadratic_coverage (m parity : ℕ) (hp : parity = 0 ∨ parity = 1)
+    (p : Point (2 * m + 1)) (hcolor : InColor parity p) :
+    fourCoverage (oddQuadraticWeights m parity) p = 16 * (m : ℚ) ^ 2 := by
+  have hsum : (sumIndex p).1 % 2 = parity % 2 := by
+    simpa [sumIndex, InColor] using hcolor
+  have hdiff : (differenceIndex p).1 % 2 = parity % 2 := by
+    rcases hp with rfl | rfl <;>
+      simp [differenceIndex, InColor] at hcolor ⊢ <;> omega
+  have hy : p.2.1 ≤ 2 * m := by omega
+  unfold fourCoverage oddQuadraticWeights
+  dsimp
+  rw [if_pos hsum, if_pos hdiff]
+  simp only [oddCap, sumIndex, differenceIndex]
+  push_cast [Nat.cast_sub hy]
+  ring
+
+/-- Constant coverage on an even board. -/
+theorem evenQuadratic_coverage (m parity : ℕ) (hp : parity = 0 ∨ parity = 1)
+    (hm : 1 ≤ m) (p : Point (2 * m)) (hcolor : InColor parity p) :
+    fourCoverage (evenQuadraticWeights m parity) p =
+      4 * ((2 * m : ℚ) - 1) ^ 2 := by
+  have hsum : (sumIndex p).1 % 2 = parity % 2 := by
+    simpa [sumIndex, InColor] using hcolor
+  have hdiff : (differenceIndex p).1 % 2 = (parity + 1) % 2 := by
+    rcases hp with rfl | rfl <;>
+      simp [differenceIndex, InColor] at hcolor ⊢ <;> omega
+  have hy : p.2.1 ≤ 2 * m - 1 := by omega
+  have htwo : 1 ≤ 2 * m := by omega
+  have hcast : (((2 * m - 1 : ℕ) : ℚ)) = 2 * (m : ℚ) - 1 := by
+    rw [Nat.cast_sub htwo]
+    norm_num
+  unfold fourCoverage evenQuadraticWeights
+  dsimp
+  rw [if_pos hsum, if_pos hdiff]
+  simp only [evenCap, sumIndex, differenceIndex]
+  push_cast [Nat.cast_sub hy]
+  rw [hcast]
+  ring
+
+end Checkerboard
diff --git a/lakefile.lean b/lakefile.lean
new file mode 100644
index 00000000..7de55dbf
--- /dev/null
+++ b/lakefile.lean
@@ -0,0 +1,11 @@
+import Lake
+open Lake DSL
+
+package «checkerboard-verification» where
+  version := v!"0.1.0"
+
+require mathlib from git
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.32.0"
+
+lean_lib Checkerboard where
+  roots := #[`Checkerboard]
diff --git a/lean-toolchain b/lean-toolchain
new file mode 100644
index 00000000..94b9f495
--- /dev/null
+++ b/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.32.0