diff --git a/LeanPool/LatinQuarter.lean b/LeanPool/LatinQuarter.lean
new file mode 100644
index 0000000000..e688daaf25
--- /dev/null
+++ b/LeanPool/LatinQuarter.lean
@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import LeanPool.LatinQuarter.Textbook
+
+/-!
+# The smallest critical set in a Latin square
+
+Source: arxiv:2610.18199, url:https://github.com/RichardBean/latin-quarter-lean/tree/9997439dee62e1ede0aa995ddb7160dbceeff7b7
+Authors: Richard Bean
+Status: verified
+Main declarations: `LatinQuarter.Textbook.completions_even`, `LatinQuarter.Textbook.scs_eq_quarter`
+Tags: combinatorics, latin-squares, critical-sets, parity
+MSC: 05B15
+-/
+
+/-!
+# Critical sets of Latin squares
+
+Adapted from RichardBean/latin-quarter-lean at 9997439dee62e1ede0aa995ddb7160dbceeff7b7.
+Upstream NOTICE:
+
+The smallest critical set in a Latin square: Lean 4 formalization
+Copyright 2026 Richard Bean
+
+Licensed under the Apache License, Version 2.0. See LICENSE.
+
+This formalization and its documentation were substantially AI-generated
+with Codex under Richard Bean's direction. The version 0.2.0 additions
+(LatinQuarter/Parity.lean, LatinQuarter/Textbook.lean, and the kernel-replay
+and nanoda checks in the GitHub workflow) were written by Claude (Anthropic)
+at Richard Bean's request. The mathematical manuscript was
+developed with substantial assistance from Codex and Claude. See README.md.
+
+Dependencies retain their own licences; dependency sources and compiled
+libraries are not included in this source distribution.
+
+The complete modular proof is preserved, including general results about matrix minors,
+square-zero ideals, and polynomial coefficients. The duplicate standalone compilation
+and upstream audit scripts are not imported.
+-/
diff --git a/LeanPool/LatinQuarter/Basic.lean b/LeanPool/LatinQuarter/Basic.lean
new file mode 100644
index 0000000000..10ffda1661
--- /dev/null
+++ b/LeanPool/LatinQuarter/Basic.lean
@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import Mathlib.Data.Fintype.Pi
+
+/-!
+# Latin squares and defining sets
+
+Coordinates and symbols are labelled. A defining set specifies the symbols
+of a fixed Latin square on a finite set of cells. No unproved mathematical
+hypotheses are incorporated into these definitions.
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+
+/-- A labelled row-column position in an order-`n` square. -/
+abbrev Cell (n : ℕ) := Fin n × Fin n
+/-- A symbol assignment to every labelled cell, before imposing the Latin condition. -/
+abbrev Square (n : ℕ) := Fin n → Fin n → Fin n
+
+/-- Every row and column contains every symbol exactly once. -/
+def IsLatin {n : ℕ} (L : Square n) : Prop :=
+  (∀ r, Function.Bijective (L r)) ∧
+  (∀ c, Function.Bijective (fun r => L r c))
+
+/-- The square `M` retains the clues that `L` gives on `P`. -/
+def Agrees {n : ℕ} (P : Finset (Cell n)) (L M : Square n) : Prop :=
+  ∀ p ∈ P, M p.1 p.2 = L p.1 p.2
+
+/-- The Latin square `L` is uniquely determined by its entries on `P`. -/
+def IsDefining {n : ℕ} (P : Finset (Cell n)) (L : Square n) : Prop :=
+  IsLatin L ∧ ∀ M, IsLatin M → Agrees P L M → M = L
+
+/-- All labelled Latin squares extending the specified clues from `L`. -/
+noncomputable def completions {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) : Finset (Square n) := by
+  classical
+  exact Finset.univ.filter (fun M => IsLatin M ∧ Agrees P L M)
+
+@[simp] theorem mem_completions {n : ℕ} {P : Finset (Cell n)}
+    {L M : Square n} :
+    M ∈ completions P L ↔ IsLatin M ∧ Agrees P L M := by
+  classical
+  simp [completions]
+
+theorem defining_iff_completions_eq_singleton {n : ℕ}
+    (P : Finset (Cell n)) (L : Square n) :
+    IsDefining P L ↔ completions P L = {L} := by
+  classical
+  constructor
+  · rintro ⟨hL, hu⟩
+    ext M
+    simp only [mem_completions, Finset.mem_singleton]
+    constructor
+    · rintro ⟨hM, ha⟩
+      exact hu M hM ha
+    · rintro rfl
+      exact ⟨hL, fun _ _ => rfl⟩
+  · intro h
+    have hL : L ∈ completions P L := by simp [h]
+    refine ⟨(mem_completions.mp hL).1, ?_⟩
+    intro M hM ha
+    have hm : M ∈ completions P L := mem_completions.mpr ⟨hM, ha⟩
+    simpa [h] using hm
+
+theorem defining_completion_count {n : ℕ} {P : Finset (Cell n)}
+    {L : Square n} (h : IsDefining P L) :
+    (completions P L).card = 1 := by
+  rw [(defining_iff_completions_eq_singleton P L).mp h]
+  exact Finset.card_singleton L
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/Budget.lean b/LeanPool/LatinQuarter/Budget.lean
new file mode 100644
index 0000000000..7258cf04d2
--- /dev/null
+++ b/LeanPool/LatinQuarter/Budget.lean
@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import Mathlib.Tactic.Linarith
+public import LeanPool.LatinQuarter.Rows
+
+/-!
+# The global clue budget
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+open scoped BigOperators
+
+theorem quarter_eq (n : ℕ) : n * n / 4 = (n / 2) * (n - n / 2) := by
+  have hn : n = 2 * (n / 2) + n % 2 := by omega
+  have hk : n / 2 ≤ n := by omega
+  have hsub : n - n / 2 + n / 2 = n := Nat.sub_add_cancel hk
+  have he : n * n = 4 * ((n / 2) * (n - n / 2)) + n % 2 := by
+    have hm : n % 2 = 0 ∨ n % 2 = 1 := by omega
+    rcases hm with hm | hm <;> rw [hm] at hn ⊢ <;> nlinarith
+  omega
+
+theorem sum_free_columns {n : ℕ} (P : Finset (Cell n)) :
+    (∑ r, Fintype.card (FreeColumn P r)) + P.card = n * n := by
+  classical
+  let e : ((r : Fin n) × FreeColumn P r) ≃ {p : Cell n // p ∉ P} :=
+    { toFun := fun x => ⟨(x.1, x.2.val), x.2.property⟩
+      invFun := fun x => ⟨x.val.1, ⟨x.val.2, x.property⟩⟩
+      left_inv := fun x => by cases x; rfl
+      right_inv := fun x => by cases x; rfl }
+  have hc := Fintype.card_congr e
+  rw [Fintype.card_sigma, Fintype.card_subtype_compl] at hc
+  simp only [Fintype.card_prod, Fintype.card_fin, Fintype.card_coe] at hc
+  have hp : P.card ≤ n * n := by
+    simpa using (Finset.card_le_univ P)
+  omega
+
+/-- The global clue budget supplies exactly the strict inequality used
+by the residual-position pigeonhole argument. -/
+theorem clue_budget {n : ℕ} (P : Finset (Cell n))
+    (hP : P.card < n * n / 4) :
+    (n - n / 2) * (n - n / 2) <
+      ∑ r, (Fintype.card (FreeColumn P r) - n / 2) := by
+  have hs := sum_free_columns P
+  have hb := Finset.sum_le_sum (s := (Finset.univ : Finset (Fin n)))
+    (f := fun r => Fintype.card (FreeColumn P r))
+    (g := fun r => Fintype.card (FreeColumn P r) - n / 2 + n / 2)
+    (fun r _ => by omega)
+  rw [Finset.sum_add_distrib] at hb
+  simp only [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul] at hb
+  rw [quarter_eq] at hP
+  have hk : n / 2 ≤ n := by omega
+  have hn : n = n / 2 + (n - n / 2) := by omega
+  nlinarith
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/CornerSize.lean b/LeanPool/LatinQuarter/CornerSize.lean
new file mode 100644
index 0000000000..69db3bbcbb
--- /dev/null
+++ b/LeanPool/LatinQuarter/CornerSize.lean
@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import LeanPool.LatinQuarter.Cyclic
+public import LeanPool.LatinQuarter.Budget
+
+/-!
+# Counting the two corner triangles
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+
+/-- Fold the two corner triangles into a rectangle with `n/2` rows and
+`n-n/2` columns. Their images lie on opposite sides of its anti-diagonal. -/
+theorem cornerSet_card_le (n : ℕ) : (cornerSet n).card ≤ n * n / 4 := by
+  classical
+  have hk : n / 2 ≤ n := by omega
+  have hh : n - n / 2 ≤ n / 2 + 1 := by omega
+  have hkh : n / 2 ≤ n - n / 2 := by omega
+  let f : {p : Cell n // p ∈ cornerSet n} → Fin (n / 2) × Fin (n - n / 2) :=
+    fun p => if hp : p.val.1.val + p.val.2.val < n / 2 then
+      (⟨p.val.1.val, by omega⟩, ⟨p.val.2.val, by omega⟩)
+    else
+      (⟨p.val.1.val - (n - n / 2), by
+        have hr := p.val.1.isLt
+        have hc := p.val.2.isLt
+        have hm := (mem_cornerSet _ _).mp p.property
+        omega⟩,
+       ⟨p.val.2.val - n / 2, by
+        have hr := p.val.1.isLt
+        have hc := p.val.2.isLt
+        have hm := (mem_cornerSet _ _).mp p.property
+        omega⟩)
+  have hf : Function.Injective f := by
+    rintro ⟨⟨pr, pc⟩, hp⟩ ⟨⟨qr, qc⟩, hq⟩ he
+    have hp' := (mem_cornerSet pr pc).mp hp
+    have hq' := (mem_cornerSet qr qc).mp hq
+    have hpr := pr.isLt
+    have hpc := pc.isLt
+    have hqr := qr.isLt
+    have hqc := qc.isLt
+    dsimp [f] at he
+    split_ifs at he with hp0 hq0 hq0
+    all_goals
+      have he1 := congrArg (fun x : Fin (n / 2) × Fin (n - n / 2) => x.1.val) he
+      have he2 := congrArg (fun x : Fin (n / 2) × Fin (n - n / 2) => x.2.val) he
+      simp only at he1 he2
+      apply Subtype.ext
+      change (pr, pc) = (qr, qc)
+      apply Prod.ext <;> apply Fin.ext <;> dsimp only at * <;> omega
+  have hc := Fintype.card_le_of_injective f hf
+  rw [quarter_eq]
+  simpa only [Fintype.card_coe, Fintype.card_prod, Fintype.card_fin] using hc
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/Counting.lean b/LeanPool/LatinQuarter/Counting.lean
new file mode 100644
index 0000000000..3de888a287
--- /dev/null
+++ b/LeanPool/LatinQuarter/Counting.lean
@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import LeanPool.LatinQuarter.Rows
+public import LeanPool.LatinQuarter.Tags
+public import LeanPool.LatinQuarter.SquareZero
+
+/-!
+# Polynomial coefficients count Latin completions
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+open scoped BigOperators Matrix
+open MvPolynomial
+
+/-- The factors contributed by the filled cells to the completion polynomial. -/
+noncomputable def clueProduct {n : ℕ} {R : Type*} [CommRing R]
+    (P : Finset (Cell n)) (L : Square n) (Y : Matrix (Fin n) (Fin n) R) : R := by
+  classical
+  exact ∏ r, ∏ c : {c : Fin n // (r, c) ∈ P}, Y c (L r c)
+
+/-- The product of row matching determinants over the unfilled cells. -/
+noncomputable def rowMinorProduct {n : ℕ} {R : Type*} [CommRing R]
+    (P : Finset (Cell n)) (L : Square n) (Y : Matrix (Fin n) (Fin n) R) : R := by
+  classical
+  exact ∏ r, (Y.submatrix (fun c : FreeColumn P r => c.val)
+    (fun c : FreeColumn P r => L r c)).det
+
+/-- Expanding the row matching sums enumerates all independent ways to
+finish the rows. The clue factors restore the full set of cells. -/
+theorem expand_row_matchings {n : ℕ} {R : Type*} [CommRing R] [CharP R 2]
+    (P : Finset (Cell n)) (L : Square n) (Y : Matrix (Fin n) (Fin n) R) :
+    clueProduct P L Y * rowMinorProduct P L Y =
+      ∑ σ : RowChoices P, ∏ p : Cell n, Y p.2 (chosenSquare P L σ p.1 p.2) := by
+  classical
+  unfold rowMinorProduct
+  simp_rw [det_eq_matching_sum]
+  rw [Fintype.prod_sum, Finset.mul_sum]
+  apply Finset.sum_congr rfl
+  intro σ _
+  rw [Fintype.prod_prod_type]
+  unfold clueProduct
+  rw [← Finset.prod_mul_distrib]
+  apply Finset.prod_congr rfl
+  intro r _
+  have hp := Fintype.prod_subtype_mul_prod_subtype (fun c : Fin n => (r, c) ∈ P)
+    (fun c => Y c (chosenSquare P L σ r c))
+  convert hp using 1
+  · apply congrArg₂ (· * ·)
+    · apply Finset.prod_congr rfl
+      intro c _
+      rw [chosenSquare_clue P L σ r c c.property]
+    · apply Finset.prod_congr rfl
+      intro c _
+      simp only [Matrix.submatrix_apply, chosenSquare_free]
+
+/-- The column-symbol position recording a cell's contribution to its monomial. -/
+abbrev columnSymbol {n : ℕ} (M : Square n) (p : Cell n) : Cell n :=
+  (p.2, M p.1 p.2)
+
+theorem columnSymbol_bijective {n : ℕ} {M : Square n} (hM : IsLatin M) :
+    Function.Bijective (columnSymbol M) := by
+  apply Function.Injective.bijective_of_finite
+  intro p q hpq
+  have hc : p.2 = q.2 := congrArg Prod.fst hpq
+  have hs : M p.1 p.2 = M q.1 q.2 := congrArg Prod.snd hpq
+  apply Prod.ext
+  · apply (hM.2 p.2).injective
+    simpa only [columnSymbol, ← hc] using hs
+  · exact hc
+
+theorem isLatin_of_columnSymbol_injective {n : ℕ} {M : Square n}
+    (hr : ∀ r, Function.Bijective (M r)) (hi : Function.Injective (columnSymbol M)) :
+    IsLatin M := by
+  refine ⟨hr, fun c => Function.Injective.bijective_of_finite ?_⟩
+  intro r s h
+  have he : columnSymbol M (r, c) = columnSymbol M (s, c) := Prod.ext rfl h
+  exact congrArg Prod.fst (hi he)
+
+open Classical in
+/-- The full square-free coefficient is one for a Latin square and zero
+for a row permutation that repeats a symbol in a column. -/
+theorem full_coefficient {n : ℕ} (M : Square n)
+    (hr : ∀ r, Function.Bijective (M r)) :
+    (∏ p : Cell n, X (columnSymbol M p) : MvPolynomial (Cell n) (ZMod 2)).coeff
+      (allTagsExponent (Cell n)) =
+      if IsLatin M then 1 else 0 := by
+  classical
+  by_cases hM : IsLatin M
+  · rw [ite_eq_left hM]
+    have hp := (Equiv.ofBijective (columnSymbol M) (columnSymbol_bijective hM)).prod_comp
+      (fun p => (X p : MvPolynomial (Cell n) (ZMod 2)))
+    change (∏ p, X (columnSymbol M p) : MvPolynomial (Cell n) (ZMod 2)) = ∏ p, X p at hp
+    rw [hp]
+    exact coeff_allTags_product
+  · rw [ite_eq_right hM]
+    have hn : ¬ Function.Injective (columnSymbol M) :=
+      fun hi => hM (isLatin_of_columnSymbol_injective hr hi)
+    simp only [Function.Injective, not_forall] at hn
+    obtain ⟨p, q, hpq⟩ := hn
+    have he : columnSymbol M p = columnSymbol M q := by tauto
+    have hne : p ≠ q := by tauto
+    apply squarefree_coeff_zero_of_quotient_zero _ (by simp)
+    simp only [map_prod]
+    change (∏ p : Cell n, tag (columnSymbol M p)) = 0
+    exact product_eq_zero_of_repeated_square_zero _ hne (congrArg tag he) (tag_sq _)
+
+open Classical in
+/-- The highest square-free coefficient counts the Latin row choices modulo two. -/
+theorem coefficient_eq_sum_latin_choices {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (hL : IsLatin L) (a : Cell n → ZMod 2) :
+    (clueProduct P L (Matrix.of fun c s => X (c, s) + C (a (c, s))) *
+      rowMinorProduct P L (Matrix.of fun c s => X (c, s) + C (a (c, s)))).coeff
+      (allTagsExponent (Cell n)) =
+      ∑ σ : RowChoices P, if IsLatin (chosenSquare P L σ) then (1 : ZMod 2) else 0 := by
+  classical
+  rw [expand_row_matchings, coeff_sum]
+  apply Finset.sum_congr rfl
+  intro σ _
+  change (∏ p : Cell n, (X (columnSymbol (chosenSquare P L σ) p) +
+    C (a (columnSymbol (chosenSquare P L σ) p)))).coeff (allTagsExponent (Cell n)) = _
+  rw [coeff_prod_add_constants _ _ _ (by simp)]
+  exact full_coefficient _ (chosenSquare_rows P L hL σ)
+
+/-- Adding constants preserves the completion coefficient, and unique
+completion makes that coefficient exactly one. -/
+theorem defining_coefficient_one {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (h : IsDefining P L) (a : Cell n → ZMod 2) :
+    (clueProduct P L (Matrix.of fun c s => X (c, s) + C (a (c, s))) *
+      rowMinorProduct P L (Matrix.of fun c s => X (c, s) + C (a (c, s)))).coeff
+      (allTagsExponent (Cell n)) = 1 := by
+  classical
+  rw [coefficient_eq_sum_latin_choices P L h.1 a]
+  rw [Finset.sum_eq_single (1 : RowChoices P)]
+  · simp [h.1]
+  · intro σ _ hσ
+    rw [ite_eq_right]
+    exact fun hl => hσ (unique_chosenSquare P L h σ hl)
+  · simp
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/Cyclic.lean b/LeanPool/LatinQuarter/Cyclic.lean
new file mode 100644
index 0000000000..2c1a62ed15
--- /dev/null
+++ b/LeanPool/LatinQuarter/Cyclic.lean
@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import Mathlib.Algebra.Group.Fin.Basic
+public import Mathlib.Data.Fintype.Prod
+public import Mathlib.Tactic.Linarith
+public import LeanPool.LatinQuarter.Basic
+
+/-!
+# The cyclic Latin square and its corner set
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+
+/-- The addition table of `Fin n`, used to attain the critical-set bound. -/
+def cyclic (n : ℕ) : Square n := fun r c => r + c
+
+theorem cyclic_isLatin (n : ℕ) (hn : 0 < n) : IsLatin (cyclic n) := by
+  let : NeZero n := ⟨by omega⟩
+  exact ⟨fun r => (Equiv.addLeft r).bijective, fun c => (Equiv.addRight c).bijective⟩
+
+/-- The two opposite triangular corners in the cyclic Latin square. -/
+def cornerSet (n : ℕ) : Finset (Cell n) :=
+  Finset.univ.filter (fun p => p.1.val + p.2.val < n / 2 ∨
+    n + n / 2 ≤ p.1.val + p.2.val)
+
+@[simp] theorem mem_cornerSet {n : ℕ} (r c : Fin n) :
+    (r, c) ∈ cornerSet n ↔ r.val + c.val < n / 2 ∨
+      n + n / 2 ≤ r.val + c.val := by simp [cornerSet]
+
+/-- Rows are visited from top to bottom, and each row from right to left. -/
+def fillingOrder {n : ℕ} (r c : Fin n) : ℕ := r.val * n + (n - 1 - c.val)
+
+theorem fillingOrder_row {n : ℕ} (r i c d : Fin n) (hi : i < r) :
+    fillingOrder i d < fillingOrder r c := by
+  have hn := c.isLt
+  have hd := d.isLt
+  have hi' : i.val + 1 ≤ r.val := hi
+  have hm := Nat.mul_le_mul_right n hi'
+  have hrem : n - 1 - d.val < n := by omega
+  unfold fillingOrder
+  nlinarith
+
+theorem fillingOrder_column {n : ℕ} (r c j : Fin n) (hj : c < j) :
+    fillingOrder r j < fillingOrder r c := by
+  have hc := c.isLt
+  have hjn := j.isLt
+  unfold fillingOrder
+  omega
+
+/-- Every non-corner cell is forced by the cells preceding it. -/
+theorem corner_forcing_step {n : ℕ} (hn : 0 < n) (M : Square n)
+    (hM : IsLatin M) (ha : Agrees (cornerSet n) (cyclic n) M)
+    (r c : Fin n)
+    (hprev : ∀ i j, fillingOrder i j < fillingOrder r c → M i j = cyclic n i j) :
+    M r c = cyclic n r c := by
+  classical
+  by_cases hrc : (r, c) ∈ cornerSet n
+  · exact ha (r, c) hrc
+  have hL := cyclic_isLatin n hn
+  obtain ⟨j, hj⟩ := (hL.1 r).surjective (M r c)
+  by_cases hjc : j = c
+  · simpa [hjc] using hj.symm
+  have hrow : M r j ≠ M r c := fun he => hjc ((hM.1 r).injective he)
+  by_cases hjright : c < j
+  · have he := hprev r j (fillingOrder_column r c j hjright)
+    exact (hrow (he.trans hj)).elim
+  by_cases hrj : (r, j) ∈ cornerSet n
+  · exact (hrow ((ha (r, j) hrj).trans hj)).elim
+  have hjlt : j.val < c.val := by
+    have hne : j.val ≠ c.val := fun he => hjc (Fin.ext he)
+    change ¬c.val < j.val at hjright
+    omega
+  have hband : n / 2 ≤ r.val + j.val ∧ r.val + j.val < n + n / 2 := by
+    simpa only [mem_cornerSet, not_or, not_lt, not_le] using hrj
+  let u := r.val + j.val
+  by_cases huc : c.val ≤ u
+  · let i : Fin n := ⟨u - c.val, by have := r.isLt; dsimp [u]; omega⟩
+    have hir : i < r := by change u - c.val < r.val; dsimp [u]; omega
+    have hiadd : cyclic n i c = cyclic n r j := by
+      apply Fin.ext
+      change (i.val + c.val) % n = (r.val + j.val) % n
+      have he : i.val + c.val = r.val + j.val := by dsimp [i, u]; omega
+      rw [he]
+    have he := hprev i c (fillingOrder_row r i c c hir)
+    have hirEq := (hM.2 c).injective (he.trans (hiadd.trans hj))
+    exact (ne_of_lt hir hirEq).elim
+  · let i : Fin n := ⟨u + n - c.val, by have := c.isLt; omega⟩
+    have hiadd : cyclic n i c = cyclic n r j := by
+      apply Fin.ext
+      change (i.val + c.val) % n = (r.val + j.val) % n
+      have he : i.val + c.val = u + n := by have := c.isLt; dsimp [i]; omega
+      rw [he, Nat.add_mod_right]
+    have hic : (i, c) ∈ cornerSet n := by
+      apply (mem_cornerSet i c).mpr
+      right
+      have := c.isLt
+      dsimp [i, u]
+      omega
+    have hirEq := (hM.2 c).injective ((ha (i, c) hic).trans (hiadd.trans hj))
+    have he : cyclic n r c = cyclic n r j := by
+      change i = r at hirEq
+      rw [hirEq] at hiadd
+      exact hiadd
+    exact (hjc ((hL.1 r).injective he).symm).elim
+
+theorem cornerSet_isDefining (n : ℕ) (hn : 0 < n) :
+    IsDefining (cornerSet n) (cyclic n) := by
+  refine ⟨cyclic_isLatin n hn, ?_⟩
+  intro M hM ha
+  have all : ∀ m : ℕ, ∀ r c : Fin n, fillingOrder r c = m → M r c = cyclic n r c := by
+    intro m
+    induction m using Nat.strong_induction_on with
+    | h m ih =>
+      intro r c hrc
+      apply corner_forcing_step hn M hM ha r c
+      intro i j hij
+      exact ih (fillingOrder i j) (by omega) i j rfl
+  funext r c
+  exact all _ r c rfl
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/Imports.lean b/LeanPool/LatinQuarter/Imports.lean
new file mode 100644
index 0000000000..dd676c378d
--- /dev/null
+++ b/LeanPool/LatinQuarter/Imports.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2026 Lean Pool contributors. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Lean Pool contributors
+-/
+module  -- shake: keep-all --deprecated_module: ignore
+
+-- Generated project imports; run `lake exe mk_all`.
+public import LeanPool.LatinQuarter
+public import LeanPool.LatinQuarter.Basic
+public import LeanPool.LatinQuarter.Budget
+public import LeanPool.LatinQuarter.CornerSize
+public import LeanPool.LatinQuarter.Counting
+public import LeanPool.LatinQuarter.Cyclic
+public import LeanPool.LatinQuarter.LowerBound
+public import LeanPool.LatinQuarter.Main
+public import LeanPool.LatinQuarter.Minors
+public import LeanPool.LatinQuarter.Parity
+public import LeanPool.LatinQuarter.Rows
+public import LeanPool.LatinQuarter.Shifted
+public import LeanPool.LatinQuarter.SquareZero
+public import LeanPool.LatinQuarter.Tags
+public import LeanPool.LatinQuarter.Textbook
+public import LeanPool.LatinQuarter.Vanishing
diff --git a/LeanPool/LatinQuarter/LowerBound.lean b/LeanPool/LatinQuarter/LowerBound.lean
new file mode 100644
index 0000000000..9707277f83
--- /dev/null
+++ b/LeanPool/LatinQuarter/LowerBound.lean
@@ -0,0 +1,61 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import LeanPool.LatinQuarter.Counting
+public import LeanPool.LatinQuarter.Shifted
+public import LeanPool.LatinQuarter.Budget
+
+/-!
+# The lower bound for defining sets
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+open scoped BigOperators Matrix
+open MvPolynomial
+
+/-- Below the quarter bound, any balanced choice of marked positions makes the
+completion polynomial's highest square-free coefficient vanish. No Latin condition
+on the reference square is required. -/
+theorem small_clue_coefficient_zero {n : ℕ} (P : Finset (Cell n)) (L : Square n)
+    (e : Fin (n / 2) ⊕ Fin (n - n / 2) ≃ Fin n) (hP : P.card < n * n / 4) :
+    (clueProduct P L (Matrix.of fun c s => X (c, s) + C (markedConstant e c s)) *
+      rowMinorProduct P L (Matrix.of fun c s => X (c, s) + C (markedConstant e c s))).coeff
+      (allTagsExponent (Cell n)) = 0 := by
+  classical
+  let Y : Matrix (Fin n) (Fin n) (MvPolynomial (Cell n) (ZMod 2)) :=
+    fun c s => X (c, s) + C (markedConstant e c s)
+  let q := Ideal.Quotient.mk (repeatedTagIdeal (Cell n))
+  have hrow : q (rowMinorProduct P L Y) = rowMinorProduct P L (shiftedTags e) := by
+    unfold rowMinorProduct
+    rw [map_prod]
+    apply Finset.prod_congr rfl
+    intro r _
+    rw [q.map_det]
+    congr 1
+  have hz : rowMinorProduct P L (shiftedTags e) = 0 :=
+    shifted_tags_product_vanishes e (fun r => FreeColumn P r)
+      (fun _ c => c.val) (fun r c => L r c) (clue_budget P hP)
+  have hzq : q (clueProduct P L Y * rowMinorProduct P L Y) = 0 := by
+    rw [map_mul, hrow, hz, mul_zero]
+  exact squarefree_coeff_zero_of_quotient_zero hzq (by simp)
+
+/-- Every defining set in every labelled Latin square has at least the
+quarter-square number of clues. No restriction on the completed square
+or on the distribution of its clues is assumed. -/
+theorem defining_set_lower_bound {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (h : IsDefining P L) : n * n / 4 ≤ P.card := by
+  classical
+  by_contra! hP
+  let e : Fin (n / 2) ⊕ Fin (n - n / 2) ≃ Fin n :=
+    finSumFinEquiv.trans (finCongr (by omega))
+  have hc0 := small_clue_coefficient_zero P L e hP
+  have hc1 := defining_coefficient_one P L h (fun p => markedConstant e p.1 p.2)
+  exact zero_ne_one (hc0.symm.trans hc1)
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/Main.lean b/LeanPool/LatinQuarter/Main.lean
new file mode 100644
index 0000000000..09c5eea7a5
--- /dev/null
+++ b/LeanPool/LatinQuarter/Main.lean
@@ -0,0 +1,83 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import Mathlib.Order.ConditionallyCompleteLattice.Basic
+public import LeanPool.LatinQuarter.LowerBound
+public import LeanPool.LatinQuarter.CornerSize
+
+/-!
+# The quarter bound for critical sets of Latin squares
+
+The definitions of Latin square, agreement, and unique completion are in
+`Basic.lean`. The lower bound is proved for every Latin square. The matching
+upper bound is furnished by the two corner triangles of the cyclic square.
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+
+/-- A critical set is a defining set with no proper defining subset. -/
+def IsCritical {n : ℕ} (P : Finset (Cell n)) (L : Square n) : Prop :=
+  IsDefining P L ∧ ∀ Q : Finset (Cell n), Q ⊂ P → ¬ IsDefining Q L
+
+theorem critical_set_lower_bound {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (h : IsCritical P L) : n * n / 4 ≤ P.card :=
+  defining_set_lower_bound P L h.1
+
+theorem cornerSet_card (n : ℕ) (hn : 0 < n) :
+    (cornerSet n).card = n * n / 4 := by
+  apply le_antisymm (cornerSet_card_le n)
+  exact defining_set_lower_bound _ _ (cornerSet_isDefining n hn)
+
+theorem cornerSet_isCritical (n : ℕ) (hn : 0 < n) :
+    IsCritical (cornerSet n) (cyclic n) := by
+  refine ⟨cornerSet_isDefining n hn, ?_⟩
+  intro Q hQ hdef
+  have hlt := Finset.card_lt_card hQ
+  have hlo := defining_set_lower_bound Q (cyclic n) hdef
+  rw [cornerSet_card n hn] at hlt
+  omega
+
+/-- The smallest critical-set size among all labelled Latin squares of
+order `n`. This definition contains no bound or cyclic-square assumption. -/
+noncomputable def scs (n : ℕ) : ℕ :=
+  sInf {m : ℕ | ∃ (L : Square n) (P : Finset (Cell n)),
+    IsCritical P L ∧ P.card = m}
+
+/-- The smallest critical-set size in one specified square. -/
+noncomputable def scsOf {n : ℕ} (L : Square n) : ℕ :=
+  sInf {m : ℕ | ∃ P : Finset (Cell n), IsCritical P L ∧ P.card = m}
+
+/-- Main theorem: the least size over all Latin squares is `floor(n²/4)`. -/
+theorem scs_eq_quarter (n : ℕ) (hn : 0 < n) : scs n = n * n / 4 := by
+  apply IsLeast.csInf_eq
+  constructor
+  · exact ⟨cyclic n, cornerSet n, cornerSet_isCritical n hn, cornerSet_card n hn⟩
+  · rintro m ⟨L, P, hP, rfl⟩
+    exact critical_set_lower_bound P L hP
+
+/-- The cyclic Latin square attains the same least size. -/
+theorem cyclic_scs_eq_quarter (n : ℕ) (hn : 0 < n) :
+    scsOf (cyclic n) = n * n / 4 := by
+  apply IsLeast.csInf_eq
+  constructor
+  · exact ⟨cornerSet n, cornerSet_isCritical n hn, cornerSet_card n hn⟩
+  · rintro m ⟨P, hP, rfl⟩
+    exact critical_set_lower_bound P (cyclic n) hP
+
+/-- A single statement giving the unrestricted lower bound and an
+explicit critical set attaining it in the cyclic square. -/
+theorem quarter_bound (n : ℕ) (hn : 0 < n) :
+    (∀ (L : Square n) (P : Finset (Cell n)),
+      IsDefining P L → n * n / 4 ≤ P.card) ∧
+    IsCritical (cornerSet n) (cyclic n) ∧
+    (cornerSet n).card = n * n / 4 :=
+  ⟨fun L P h => defining_set_lower_bound P L h,
+    cornerSet_isCritical n hn, cornerSet_card n hn⟩
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/Minors.lean b/LeanPool/LatinQuarter/Minors.lean
new file mode 100644
index 0000000000..f6c83d52b7
--- /dev/null
+++ b/LeanPool/LatinQuarter/Minors.lean
@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
+public import Mathlib.LinearAlgebra.Matrix.Block
+public import Mathlib.RingTheory.Ideal.Operations
+
+/-!
+# Matrix minors in ideals
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+
+open scoped BigOperators Matrix
+
+variable {R : Type*} [CommRing R]
+
+/-- All minors of size `t` lie in `J`. Repeated indices are allowed;
+their determinants are zero. -/
+def AllMinorsIn {m n : Type*} (M : Matrix m n R) (t : ℕ) (J : Ideal R) : Prop :=
+  ∀ (r : Fin t → m) (c : Fin t → n), (M.submatrix r c).det ∈ J
+
+theorem allMinorsIn_mul_left {m n p : Type*} [Fintype n]
+    (A : Matrix m n R) (B : Matrix n p R) {t : ℕ} {J : Ideal R}
+    (hB : AllMinorsIn B t J) : AllMinorsIn (A * B) t J := by
+  classical
+  intro r c
+  have heq : (A * B).submatrix r c =
+      fun i => ∑ j, A (r i) j • (fun l => B j (c l)) := by
+    ext i l
+    simp [Matrix.mul_apply, Finset.sum_apply, Pi.smul_apply, smul_eq_mul]
+  rw [heq]
+  change Matrix.detRowAlternating.toMultilinearMap
+    (fun i => ∑ j, A (r i) j • (fun l => B j (c l))) ∈ J
+  rw [MultilinearMap.map_sum]
+  apply Submodule.sum_mem
+  intro f _
+  rw [MultilinearMap.map_smul_univ]
+  exact J.smul_mem _ (hB f c)
+
+theorem allMinorsIn_transpose {m n : Type*} (M : Matrix m n R)
+    {t : ℕ} {J : Ideal R} (hM : AllMinorsIn M t J) :
+    AllMinorsIn M.transpose t J := by
+  intro r c
+  simpa only [← Matrix.transpose_submatrix, Matrix.det_transpose] using hM c r
+
+theorem allMinorsIn_mul_right {m n p : Type*} [Fintype n]
+    (A : Matrix m n R) (B : Matrix n p R) {t : ℕ} {J : Ideal R}
+    (hA : AllMinorsIn A t J) : AllMinorsIn (A * B) t J := by
+  have h := allMinorsIn_mul_left B.transpose A.transpose (allMinorsIn_transpose A hA)
+  have h' := allMinorsIn_transpose (B.transpose * A.transpose) h
+  simpa only [Matrix.transpose_mul, Matrix.transpose_transpose] using h'
+
+/-- A determinant with `s.card` rows in an ideal lies in that ideal power. -/
+theorem det_mem_pow_of_rows {ι : Type*} [Fintype ι] [DecidableEq ι]
+    (M : Matrix ι ι R) (J : Ideal R) (s : Finset ι)
+    (h : ∀ i ∈ s, ∀ j, M i j ∈ J) : M.det ∈ J ^ s.card := by
+  classical
+  rw [← Matrix.det_transpose, Matrix.det_apply']
+  apply Submodule.sum_mem
+  intro σ _
+  apply Ideal.mul_mem_left
+  change (∏ i, M i (σ i)) ∈ J ^ s.card
+  rw [← Finset.prod_mul_prod_compl s]
+  apply Ideal.mul_mem_right
+  have hp := Ideal.prod_mem_prod (I := fun _ : ι => J) (x := fun i => M i (σ i))
+    (s := s) (fun i hi => h i hi (σ i))
+  simpa using hp
+
+/-- The lower block rows supply enough factors from the residual ideal. -/
+theorem allMinorsIn_fromBlocks_diagonal {k h t : ℕ}
+    (A : Matrix (Fin k) (Fin k) R) (Z : Matrix (Fin h) (Fin h) R)
+    (J : Ideal R) (hZ : ∀ i j, Z i j ∈ J) :
+    AllMinorsIn (Matrix.fromBlocks A 0 0 Z) t (J ^ (t - k)) := by
+  classical
+  intro r c
+  by_cases hr : Function.Injective r
+  · let s : Finset (Fin t) := Finset.univ.filter (fun i => (r i).isRight)
+    have htop : sᶜ.card ≤ k := by
+      have hsub : sᶜ.image r ⊆
+          Finset.univ.map (Function.Embedding.inl : Fin k ↪ Fin k ⊕ Fin h) := by
+        intro x hx
+        obtain ⟨i, hi, rfl⟩ := Finset.mem_image.mp hx
+        cases he : r i with
+        | inl a => simp
+        | inr b => simp [s, he] at hi
+      have hc := Finset.card_le_card hsub
+      simpa [Finset.card_image_of_injective _ hr] using hc
+    have hs : t - k ≤ s.card := by
+      have hc := Finset.card_add_card_compl s
+      simp only [Fintype.card_fin] at hc
+      omega
+    apply Ideal.pow_le_pow_right hs
+    apply det_mem_pow_of_rows _ J s
+    intro i hi j
+    have hir : (r i).isRight := (Finset.mem_filter.mp hi).2
+    cases he : r i with
+    | inl a => simp [he] at hir
+    | inr b =>
+      cases hc : c j with
+      | inl a => simp [Matrix.submatrix, he, hc]
+      | inr d => simpa [Matrix.submatrix, he, hc] using hZ b d
+  · simp only [Function.Injective, not_forall] at hr
+    obtain ⟨a, b, hab⟩ := hr
+    have he : r a = r b := by tauto
+    have hn : a ≠ b := by tauto
+    rw [Matrix.det_zero_of_row_eq hn (by ext j; simp [Matrix.submatrix, he])]
+    exact Ideal.zero_mem _
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/Parity.lean b/LeanPool/LatinQuarter/Parity.lean
new file mode 100644
index 0000000000..75b8510ff1
--- /dev/null
+++ b/LeanPool/LatinQuarter/Parity.lean
@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import LeanPool.LatinQuarter.LowerBound
+
+/-!
+# Parity of the number of completions
+
+Written by Claude (Anthropic) at Richard Bean's request, October 2026, for
+version 0.2.0. This is Theorem A of the paper: below the quarter bound, every
+set of clues taken from a Latin square has an even number of completions.
+
+The coefficient computation in `Counting.lean` holds for every set of clues,
+not only for defining sets: the square-free coefficient counts, modulo two,
+the row choices that produce Latin squares. Those row choices correspond
+exactly to the completions. The vanishing argument used in `LowerBound.lean`
+makes the coefficient zero below the quarter bound.
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+open scoped BigOperators Matrix
+open MvPolynomial
+
+open Classical in
+/-- The square-free coefficient counts the Latin row choices modulo two. -/
+theorem coefficient_eq_card_latin_choices {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (hL : IsLatin L) (a : Cell n → ZMod 2) :
+    (clueProduct P L (Matrix.of fun c s => X (c, s) + C (a (c, s))) *
+      rowMinorProduct P L (Matrix.of fun c s => X (c, s) + C (a (c, s)))).coeff
+      (allTagsExponent (Cell n)) =
+      ((Finset.univ.filter
+        (fun σ : RowChoices P => IsLatin (chosenSquare P L σ))).card : ZMod 2) := by
+  rw [coefficient_eq_sum_latin_choices P L hL a, Finset.sum_boole]
+
+/-- Every completion arises from one permutation of the free cells in each row. -/
+theorem exists_rowChoices_of_completion {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (hL : IsLatin L) (M : Square n) (hM : IsLatin M)
+    (ha : Agrees P L M) : ∃ σ : RowChoices P, chosenSquare P L σ = M := by
+  -- In row `r`, the free cell `c` of `M` holds the symbol that `L` has in
+  -- column `(L r)⁻¹ (M r c)`, and that column is also free.
+  have hfree : ∀ (r : Fin n) (c : FreeColumn P r),
+      (r, (Equiv.ofBijective (L r) (hL.1 r)).symm (M r c)) ∉ P := by
+    intro r c hmem
+    have hLd : L r ((Equiv.ofBijective (L r) (hL.1 r)).symm (M r c)) = M r c :=
+      Equiv.ofBijective_apply_symm_apply (L r) (hL.1 r) (M r c)
+    have hMd := ha _ hmem
+    have hdc : (Equiv.ofBijective (L r) (hL.1 r)).symm (M r c) = c.val :=
+      (hM.1 r).injective (hMd.trans hLd)
+    rw [hdc] at hmem
+    exact c.property hmem
+  let f : (r : Fin n) → FreeColumn P r → FreeColumn P r := fun r c =>
+    ⟨(Equiv.ofBijective (L r) (hL.1 r)).symm (M r c), hfree r c⟩
+  have hf : ∀ r, Function.Injective (f r) := by
+    intro r c c' h
+    have h1 := congrArg Subtype.val h
+    have h2 := (Equiv.ofBijective (L r) (hL.1 r)).symm.injective h1
+    exact Subtype.ext ((hM.1 r).injective h2)
+  let σ : RowChoices P := fun r => Equiv.ofBijective (f r) (hf r).bijective_of_finite
+  refine ⟨σ, ?_⟩
+  funext r c
+  by_cases hc : (r, c) ∈ P
+  · rw [chosenSquare_clue P L σ r c hc]
+    exact (ha (r, c) hc).symm
+  · calc chosenSquare P L σ r c = L r (σ r ⟨c, hc⟩) := chosenSquare_free P L σ r ⟨c, hc⟩
+      _ = M r c := Equiv.ofBijective_apply_symm_apply (L r) (hL.1 r) (M r c)
+
+open Classical in
+/-- The completions are in bijection with the Latin row choices. -/
+theorem card_completions_eq {n : ℕ} (P : Finset (Cell n)) (L : Square n)
+    (hL : IsLatin L) :
+    (completions P L).card =
+      (Finset.univ.filter
+        (fun σ : RowChoices P => IsLatin (chosenSquare P L σ))).card := by
+  symm
+  apply Finset.card_bij (fun σ _ => chosenSquare P L σ)
+  · intro σ hσ
+    exact mem_completions.mpr ⟨(Finset.mem_filter.mp hσ).2, chosenSquare_agrees P L σ⟩
+  · intro σ _ τ _ h
+    exact chosenSquare_injective P L hL h
+  · intro M hM
+    obtain ⟨hMl, hMa⟩ := mem_completions.mp hM
+    obtain ⟨σ, hσ⟩ := exists_rowChoices_of_completion P L hL M hMl hMa
+    refine ⟨σ, Finset.mem_filter.mpr ⟨Finset.mem_univ σ, ?_⟩, hσ⟩
+    rw [hσ]
+    exact hMl
+
+/-- Theorem A, in the cell form used throughout this package: if fewer than
+`n * n / 4` cells of a Latin square `L` are given, the number of Latin squares
+that agree with `L` on those cells is even. -/
+theorem completions_card_even {n : ℕ} (P : Finset (Cell n)) (L : Square n)
+    (hL : IsLatin L) (hP : P.card < n * n / 4) :
+    Even (completions P L).card := by
+  let e : Fin (n / 2) ⊕ Fin (n - n / 2) ≃ Fin n :=
+    finSumFinEquiv.trans (finCongr (by omega))
+  have hc0 := small_clue_coefficient_zero P L e hP
+  have hc1 := coefficient_eq_card_latin_choices P L hL
+    (fun p => markedConstant e p.1 p.2)
+  rw [hc0, ← card_completions_eq P L hL] at hc1
+  exact ZMod.natCast_eq_zero_iff_even.mp hc1.symm
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/Rows.lean b/LeanPool/LatinQuarter/Rows.lean
new file mode 100644
index 0000000000..16d3439445
--- /dev/null
+++ b/LeanPool/LatinQuarter/Rows.lean
@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import Mathlib.LinearAlgebra.Matrix.Determinant.Basic
+public import Mathlib.Algebra.CharP.Two
+public import LeanPool.LatinQuarter.Basic
+
+/-!
+# Independent permutations of free row entries
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+open scoped BigOperators Matrix
+
+/-- Columns whose entries in row `r` have not been specified as clues. -/
+abbrev FreeColumn {n : ℕ} (P : Finset (Cell n)) (r : Fin n) :=
+  {c : Fin n // (r, c) ∉ P}
+
+/-- Independent permutations of the unfilled positions in each row. -/
+abbrev RowChoices {n : ℕ} (P : Finset (Cell n)) :=
+  (r : Fin n) → Equiv.Perm (FreeColumn P r)
+
+/-- Permute the symbols of each row only within its unfilled cells. -/
+noncomputable def chosenSquare {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (σ : RowChoices P) : Square n := by
+  classical
+  exact fun r c => L r ((σ r).subtypeCongr (Equiv.refl _) c)
+
+@[simp] theorem chosenSquare_free {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (σ : RowChoices P) (r : Fin n) (c : FreeColumn P r) :
+    chosenSquare P L σ r c = L r (σ r c) := by
+  classical
+  simp [chosenSquare]
+
+@[simp] theorem chosenSquare_clue {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (σ : RowChoices P) (r c : Fin n) (hc : (r, c) ∈ P) :
+    chosenSquare P L σ r c = L r c := by
+  classical
+  simp [chosenSquare, hc]
+
+@[simp] theorem chosenSquare_one {n : ℕ} (P : Finset (Cell n)) (L : Square n) :
+    chosenSquare P L 1 = L := by
+  classical
+  ext r c
+  simp [chosenSquare, Equiv.Perm.subtypeCongr.apply]
+
+theorem chosenSquare_rows {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (hL : IsLatin L) (σ : RowChoices P) :
+    ∀ r, Function.Bijective (chosenSquare P L σ r) := by
+  classical
+  intro r
+  exact (hL.1 r).comp ((σ r).subtypeCongr (Equiv.refl _)).bijective
+
+theorem chosenSquare_agrees {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (σ : RowChoices P) : Agrees P L (chosenSquare P L σ) := by
+  intro p hp
+  exact chosenSquare_clue P L σ p.1 p.2 hp
+
+theorem chosenSquare_injective {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (hL : IsLatin L) : Function.Injective (chosenSquare P L) := by
+  intro σ τ h
+  funext r
+  apply Equiv.ext
+  intro c
+  apply Subtype.ext
+  apply (hL.1 r).injective
+  have he := congrArg (fun M => M r c) h
+  simpa only [chosenSquare_free] using he
+
+theorem unique_chosenSquare {n : ℕ} (P : Finset (Cell n))
+    (L : Square n) (h : IsDefining P L) (σ : RowChoices P)
+    (hσ : IsLatin (chosenSquare P L σ)) : σ = 1 := by
+  apply chosenSquare_injective P L h.1
+  rw [chosenSquare_one]
+  exact h.2 _ hσ (chosenSquare_agrees P L σ)
+
+/-- In characteristic two the determinant is exactly the unsigned
+matching sum, written with a choice in each selected row. -/
+theorem det_eq_matching_sum {R ι : Type*} [CommRing R] [CharP R 2]
+    [Fintype ι] [DecidableEq ι] (M : Matrix ι ι R) :
+    M.det = ∑ σ : Equiv.Perm ι, ∏ i, M i (σ i) := by
+  classical
+  rw [← Matrix.det_transpose, Matrix.det_apply']
+  apply Finset.sum_congr rfl
+  intro σ _
+  have hs : (((Equiv.Perm.sign σ : ℤˣ) : ℤ) : R) = 1 := by
+    rcases Int.units_eq_one_or (Equiv.Perm.sign σ) with h | h <;>
+      simp [h, CharTwo.neg_eq]
+  rw [hs, one_mul]
+  rfl
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/Shifted.lean b/LeanPool/LatinQuarter/Shifted.lean
new file mode 100644
index 0000000000..c8f1a48db9
--- /dev/null
+++ b/LeanPool/LatinQuarter/Shifted.lean
@@ -0,0 +1,92 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import LeanPool.LatinQuarter.Vanishing
+public import LeanPool.LatinQuarter.Tags
+
+/-!
+# Shifted square-zero tags
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+open scoped BigOperators Matrix
+
+/-- The `k` dummy entries occupy distinct rows and columns, indexed by
+the left summand of `e`. -/
+noncomputable def markedConstant {N : Type*} {k h : ℕ}
+    (e : Fin k ⊕ Fin h ≃ N) (c s : N) : ZMod 2 := by
+  classical
+  exact if (e.symm c).isLeft ∧ c = s then 1 else 0
+
+/-- Square-zero bookkeeping variables with a chosen diagonal block marked by ones. -/
+noncomputable def shiftedTags {N : Type*} {k h : ℕ}
+    (e : Fin k ⊕ Fin h ≃ N) : Matrix N N (TagRing (N × N)) :=
+  fun c s => tag (c, s) + algebraMap (ZMod 2) _ (markedConstant e c s)
+
+theorem shiftedTags_square {N : Type*} {k h : ℕ}
+    (e : Fin k ⊕ Fin h ≃ N) (c s : N) :
+    squareHom (shiftedTags e c s) = algebraMap (ZMod 2) _ (markedConstant e c s) := by
+  classical
+  simp only [shiftedTags, map_add, squareHom, frobenius_def]
+  rw [pow_two, tag_sq, zero_add]
+  unfold markedConstant
+  split_ifs <;> simp
+
+/-- A version of the vanishing lemma allowing arbitrary finite sets of
+selected rows and columns in each minor. -/
+theorem shifted_tags_product_vanishes {N ι : Type*} [Fintype ι]
+    {k h : ℕ} (e : Fin k ⊕ Fin h ≃ N)
+    (α : ι → Type*) [∀ i, Fintype (α i)] [∀ i, DecidableEq (α i)]
+    (r c : (i : ι) → α i → N)
+    (hbudget : h * h < ∑ i, (Fintype.card (α i) - k)) :
+    (∏ i, ((shiftedTags e).submatrix (r i) (c i)).det) = 0 := by
+  classical
+  let M := (shiftedTags e).submatrix e e
+  let A := M.submatrix Sum.inl Sum.inl
+  let B := M.submatrix Sum.inl Sum.inr
+  let C := M.submatrix Sum.inr Sum.inl
+  let D := M.submatrix Sum.inr Sum.inr
+  have hA : squareHom.mapMatrix A = 1 := by
+    ext i j
+    change squareHom (shiftedTags e (e (Sum.inl i)) (e (Sum.inl j))) = _
+    rw [shiftedTags_square]
+    simp [markedConstant, Matrix.one_apply, e.injective.eq_iff]
+  have hC : C.map squareHom = 0 := by
+    ext i j
+    change squareHom (shiftedTags e (e (Sum.inr i)) (e (Sum.inl j))) = _
+    rw [shiftedTags_square]
+    simp [markedConstant]
+  have hD : D.map squareHom = 0 := by
+    ext i j
+    change squareHom (shiftedTags e (e (Sum.inr i)) (e (Sum.inr j))) = _
+    rw [shiftedTags_square]
+    simp [markedConstant]
+  let q (i : ι) := (Fintype.equivFin (α i)).symm
+  have hv := marked_blocks_product_vanishes A B C D hA hC hD
+    (fun i => Fintype.card (α i))
+    (fun i j => e.symm (r i (q i j)))
+    (fun i j => e.symm (c i (q i j))) hbudget
+  have hM : Matrix.fromBlocks A B C D = M := by
+    ext i j
+    cases i <;> cases j <;> rfl
+  rw [hM] at hv
+  have heq (i : ι) :
+      (M.submatrix (fun j => e.symm (r i (q i j)))
+        (fun j => e.symm (c i (q i j)))).det =
+      ((shiftedTags e).submatrix (r i) (c i)).det := by
+    have hm : M.submatrix (fun j => e.symm (r i (q i j)))
+        (fun j => e.symm (c i (q i j))) =
+        (((shiftedTags e).submatrix (r i) (c i)).submatrix (q i) (q i)) := by
+      ext a b
+      simp [M, Matrix.submatrix]
+    rw [hm, Matrix.det_submatrix_equiv_self]
+  simp_rw [heq] at hv
+  exact hv
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/SquareZero.lean b/LeanPool/LatinQuarter/SquareZero.lean
new file mode 100644
index 0000000000..8b07cf8de9
--- /dev/null
+++ b/LeanPool/LatinQuarter/SquareZero.lean
@@ -0,0 +1,64 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import Mathlib.RingTheory.Ideal.Operations
+public import Mathlib.Algebra.Algebra.Operations
+
+/-! The pigeonhole step, stated independently of Latin squares. -/
+
+@[expose] public section
+
+namespace LatinQuarter
+
+open scoped BigOperators Pointwise
+
+variable {R : Type*} [CommRing R]
+
+theorem product_eq_zero_of_repeated_square_zero
+    {ι : Type*} [Fintype ι] (f : ι → R)
+    {a b : ι} (hab : a ≠ b) (heq : f a = f b)
+    (hsq : f a * f a = 0) : ∏ i, f i = 0 := by
+  classical
+  rw [← Finset.mul_prod_erase Finset.univ f (Finset.mem_univ a)]
+  rw [← Finset.mul_prod_erase (Finset.univ.erase a) f
+    (Finset.mem_erase.mpr ⟨hab.symm, Finset.mem_univ b⟩)]
+  rw [← mul_assoc, ← heq, hsq, zero_mul]
+
+theorem product_eq_zero_of_card_lt
+    {ι κ : Type*} [Fintype ι] [Fintype κ]
+    (z : κ → R) (hz : ∀ j, z j * z j = 0)
+    (f : ι → κ) (hcard : Fintype.card κ < Fintype.card ι) :
+    ∏ i, z (f i) = 0 := by
+  have hn : ¬ Function.Injective f := by
+    intro hf
+    exact (not_le_of_gt hcard) (Fintype.card_le_of_injective f hf)
+  simp only [Function.Injective, not_forall] at hn
+  obtain ⟨a, b, hab⟩ := hn
+  have heq : f a = f b := by tauto
+  have hne : a ≠ b := by tauto
+  exact product_eq_zero_of_repeated_square_zero (fun i => z (f i))
+    hne (congrArg z heq) (hz (f a))
+
+theorem span_square_zero_pow_eq_bot
+    {κ : Type*} [Fintype κ] (z : κ → R)
+    (hz : ∀ j, z j * z j = 0) {d : ℕ}
+    (hd : Fintype.card κ < d) :
+    Ideal.span (Set.range z) ^ d = ⊥ := by
+  classical
+  apply le_antisymm _ bot_le
+  change (Submodule.span R (Set.range z)) ^ d ≤ ⊥
+  rw [Submodule.span_pow]
+  apply Submodule.span_le.mpr
+  intro x hx
+  obtain ⟨f, hf, rfl⟩ := Set.mem_pow_iff_prod.mp hx
+  choose g hg using hf
+  have hfz : f = fun i => z (g i) := funext (fun i => (hg i).symm)
+  rw [hfz]
+  have heq := product_eq_zero_of_card_lt z hz g (by simpa using hd)
+  simpa only [Submodule.mem_bot, SetLike.mem_coe] using heq
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/Tags.lean b/LeanPool/LatinQuarter/Tags.lean
new file mode 100644
index 0000000000..2f5e3bb939
--- /dev/null
+++ b/LeanPool/LatinQuarter/Tags.lean
@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import Mathlib.Algebra.CharP.Algebra
+public import Mathlib.Algebra.MvPolynomial.Degrees
+public import Mathlib.Algebra.Field.ZMod
+public import Mathlib.RingTheory.Ideal.Quotient.Operations
+public import Mathlib.RingTheory.MvPolynomial.Ideal
+
+/-!
+# Square-free polynomial coefficients
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+open scoped BigOperators
+open MvPolynomial
+
+/-- The discarded monomials: those divisible by the square of a tag. -/
+noncomputable def repeatedTagIdeal (κ : Type*) : Ideal (MvPolynomial κ (ZMod 2)) :=
+  Ideal.span ((fun d => monomial d (1 : ZMod 2)) ''
+    Set.range (fun j : κ => Finsupp.single j 2))
+
+/-- Discarding repeated tags cannot affect any square-free coefficient. -/
+theorem squarefree_coeff_zero_of_mem {κ : Type*}
+    {p : MvPolynomial κ (ZMod 2)} (hp : p ∈ repeatedTagIdeal κ)
+    {d : κ →₀ ℕ} (hd : ∀ j, d j ≤ 1) : p.coeff d = 0 := by
+  classical
+  by_contra hn
+  have hmem := mem_support_iff.mpr hn
+  obtain ⟨e, ⟨j, rfl⟩, he⟩ := mem_ideal_span_monomial_image.mp hp d hmem
+  have hj := he j
+  simp only [Finsupp.single_eq_same] at hj
+  have := hd j
+  omega
+
+theorem repeatedTagIdeal_ne_top (κ : Type*) : repeatedTagIdeal κ ≠ ⊤ := by
+  intro h
+  have hp : (1 : MvPolynomial κ (ZMod 2)) ∈ repeatedTagIdeal κ := by rw [h]; trivial
+  have hz := squarefree_coeff_zero_of_mem hp (d := 0) (by simp)
+  simp at hz
+
+/-- Polynomials modulo two, with the square of every tag set to zero. -/
+abbrev TagRing (κ : Type*) := MvPolynomial κ (ZMod 2) ⧸ repeatedTagIdeal κ
+
+instance (κ : Type*) : Nontrivial (TagRing κ) :=
+  Ideal.Quotient.nontrivial_iff.mpr (repeatedTagIdeal_ne_top κ)
+
+instance (κ : Type*) : CharP (TagRing κ) 2 :=
+  CharP.of_ringHom_of_ne_zero (algebraMap (ZMod 2) (TagRing κ)) 2 (by decide)
+
+/-- The image of a polynomial variable in the square-zero bookkeeping quotient. -/
+noncomputable def tag {κ : Type*} (j : κ) : TagRing κ :=
+  Ideal.Quotient.mk _ (X j)
+
+@[simp] theorem tag_sq {κ : Type*} (j : κ) : tag j * tag j = 0 := by
+  rw [tag, ← map_mul]
+  apply Ideal.Quotient.eq_zero_iff_mem.mpr
+  apply Ideal.subset_span
+  refine ⟨Finsupp.single j 2, ⟨j, rfl⟩, ?_⟩
+  simp [X, monomial_mul_monomial, ← Finsupp.single_add]
+
+/-- A zero polynomial in the bookkeeping ring has zero square-free
+coefficients in the original polynomial ring. -/
+theorem squarefree_coeff_zero_of_quotient_zero {κ : Type*}
+    {p : MvPolynomial κ (ZMod 2)}
+    (hp : Ideal.Quotient.mk (repeatedTagIdeal κ) p = 0)
+    {d : κ →₀ ℕ} (hd : ∀ j, d j ≤ 1) : p.coeff d = 0 :=
+  squarefree_coeff_zero_of_mem (Ideal.Quotient.eq_zero_iff_mem.mp hp) hd
+
+/-- Adding constants to `m` individual tags does not change a coefficient
+of total degree `m`. This also allows zero constants. -/
+theorem coeff_prod_add_constants {ι κ : Type*} [Fintype ι]
+    (f : ι → κ) (a : ι → ZMod 2) (d : κ →₀ ℕ)
+    (hd : ∑ j ∈ d.support, d j = Fintype.card ι) :
+    (∏ i, (X (f i) + C (a i))).coeff d = (∏ i, X (f i) : MvPolynomial κ (ZMod 2)).coeff d := by
+  classical
+  rw [Fintype.prod_add, coeff_sum]
+  rw [Finset.sum_eq_single (Finset.univ : Finset ι)]
+  · simp
+  · intro s _ hs
+    apply coeff_eq_zero_of_totalDegree_lt
+    have hc : s.card < Fintype.card ι := by
+      exact Finset.card_lt_card (Finset.ssubset_univ_iff.mpr hs)
+    have hdeg : (∏ i ∈ s, (X (f i) : MvPolynomial κ (ZMod 2))).totalDegree ≤ s.card := by
+      simpa using totalDegree_finsetProd s (fun i => (X (f i) : MvPolynomial κ (ZMod 2)))
+    have hconst : (∏ i ∈ sᶜ, C (a i) : MvPolynomial κ (ZMod 2)).totalDegree = 0 := by
+      rw [← map_prod]
+      exact totalDegree_C _
+    have hm := totalDegree_mul (∏ i ∈ s, (X (f i) : MvPolynomial κ (ZMod 2)))
+      (∏ i ∈ sᶜ, C (a i))
+    rw [hconst, add_zero] at hm
+    rw [hd]
+    exact lt_of_le_of_lt (hm.trans hdeg) hc
+  · simp
+
+/-- The exponent vector for the product of all tags, once each. -/
+noncomputable def allTagsExponent (κ : Type*) [Fintype κ] : κ →₀ ℕ :=
+  ∑ j : κ, Finsupp.single j 1
+
+@[simp] theorem allTagsExponent_apply {κ : Type*} [Fintype κ] (j : κ) :
+    allTagsExponent κ j = 1 := by
+  classical
+  simp [allTagsExponent, Finsupp.single_apply]
+
+@[simp] theorem allTagsExponent_support {κ : Type*} [Fintype κ] :
+    (allTagsExponent κ).support = Finset.univ := by
+  classical
+  ext j
+  simp
+
+theorem allTagsExponent_degree {κ : Type*} [Fintype κ] :
+    ∑ j ∈ (allTagsExponent κ).support, allTagsExponent κ j = Fintype.card κ := by
+  classical
+  simp
+
+theorem coeff_allTags_product {κ : Type*} [Fintype κ] :
+    (∏ j : κ, X j : MvPolynomial κ (ZMod 2)).coeff (allTagsExponent κ) = 1 := by
+  classical
+  have hp := prod_X_pow_eq_monomial (R := ZMod 2) (s := allTagsExponent κ)
+  simp only [allTagsExponent_support, allTagsExponent_apply, pow_one] at hp
+  rw [hp]
+  simp
+
+end LatinQuarter
diff --git a/LeanPool/LatinQuarter/Textbook.lean b/LeanPool/LatinQuarter/Textbook.lean
new file mode 100644
index 0000000000..44e3741256
--- /dev/null
+++ b/LeanPool/LatinQuarter/Textbook.lean
@@ -0,0 +1,273 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import Mathlib.SetTheory.Cardinal.Finite
+public import LeanPool.LatinQuarter.Main
+public import LeanPool.LatinQuarter.Parity
+
+/-!
+# Theorems A and B in the paper's own terms
+
+Written by Claude (Anthropic) at Richard Bean's request, October 2026, for
+version 0.2.0.
+
+This file restates Theorems A and B of the paper (Bean, arXiv:2610.18199)
+with the definitions of its Section 1, written from scratch, and derives
+them from the rest of the package. The definitions below do not use
+`IsLatin`, `Agrees`, `IsDefining`, `IsCritical` or `scs`, so a reader can
+check the claim against the paper by reading this file alone.
+
+* A Latin square of order `n` has each symbol exactly once in every row and
+  exactly once in every column. Rows, columns and symbols are `Fin n`, and
+  squares are counted with their labels.
+* A filled cell is a triple (row, column, symbol). Theorem A is stated for
+  every finite set of triples, which covers every partial Latin square. A set
+  that puts two symbols in one cell, or repeats a symbol in a row or column,
+  has no completions.
+* A completion of a set of filled cells is a Latin square that agrees with
+  every one of them, and `numCompletions T` is their number (`N(P)` in the
+  paper).
+* A defining set of `L` agrees with `L` and has `L` as its only completion.
+  It is critical if emptying any one of its filled cells leaves more than one
+  completion.
+* `scsOf L` is the smallest size of a critical set of `L`, and `scs n` is the
+  minimum of `scsOf L` over all Latin squares `L` of order `n`.
+-/
+
+@[expose] public section
+
+namespace LatinQuarter.Textbook
+
+/-- Each symbol occurs exactly once in every row and exactly once in every
+column. -/
+def Latin {n : ℕ} (L : Fin n → Fin n → Fin n) : Prop :=
+  (∀ r s, ∃! c, L r c = s) ∧ (∀ c s, ∃! r, L r c = s)
+
+/-- `L` is a completion of `T`: a Latin square that agrees with every filled
+cell (row, column, symbol) of `T`. -/
+def Completes {n : ℕ} (T : Finset (Fin n × Fin n × Fin n))
+    (L : Fin n → Fin n → Fin n) : Prop :=
+  Latin L ∧ ∀ t ∈ T, L t.1 t.2.1 = t.2.2
+
+/-- The number of completions of `T`, written `N(P)` in the paper. -/
+noncomputable def numCompletions {n : ℕ} (T : Finset (Fin n × Fin n × Fin n)) : ℕ :=
+  Nat.card {L : Fin n → Fin n → Fin n // Completes T L}
+
+/-- `T` is a defining set of `L`: `L` is a completion of `T`, and the only one. -/
+def DefiningSet {n : ℕ} (L : Fin n → Fin n → Fin n)
+    (T : Finset (Fin n × Fin n × Fin n)) : Prop :=
+  Completes T L ∧ ∀ M, Completes T M → M = L
+
+/-- A defining set of `L` is critical if emptying any one of its filled cells
+leaves more than one completion. -/
+def CriticalSet {n : ℕ} (L : Fin n → Fin n → Fin n)
+    (T : Finset (Fin n × Fin n × Fin n)) : Prop :=
+  DefiningSet L T ∧ ∀ t ∈ T, 1 < numCompletions (T.erase t)
+
+/-- `scs(L)`: the smallest number of filled cells in a critical set of `L`. -/
+noncomputable def scsOf {n : ℕ} (L : Fin n → Fin n → Fin n) : ℕ :=
+  sInf {m | ∃ T, CriticalSet L T ∧ T.card = m}
+
+/-- `scs(n)`: the minimum of `scs(L)` over all Latin squares `L` of order `n`. -/
+noncomputable def scs (n : ℕ) : ℕ :=
+  sInf {m | ∃ L : Fin n → Fin n → Fin n, Latin L ∧ scsOf L = m}
+
+/-- The cyclic square `B_n`, whose entry in cell `(r, c)` is `(r + c) mod n`. -/
+def cyclicSquare (n : ℕ) : Fin n → Fin n → Fin n :=
+  fun r c => ⟨(r.val + c.val) % n, Nat.mod_lt _ r.pos⟩
+
+/-! ## Agreement with the package's definitions -/
+
+theorem latin_iff {n : ℕ} (L : Fin n → Fin n → Fin n) : Latin L ↔ IsLatin L := by
+  simp only [Latin, IsLatin, Function.bijective_iff_existsUnique]
+
+theorem cyclicSquare_eq (n : ℕ) : cyclicSquare n = cyclic n := by
+  funext r c
+  apply Fin.ext
+  rfl
+
+/-- Once `L` completes `T`, the completions of `T` are the Latin squares that
+agree with `L` on the cells of `T`. -/
+theorem completes_iff {n : ℕ} {T : Finset (Fin n × Fin n × Fin n)}
+    {L : Fin n → Fin n → Fin n} (hL : Completes T L) (M : Fin n → Fin n → Fin n) :
+    Completes T M ↔ IsLatin M ∧ Agrees (T.image fun t => (t.1, t.2.1)) L M := by
+  constructor
+  · rintro ⟨hM, hMT⟩
+    refine ⟨(latin_iff M).mp hM, ?_⟩
+    intro p hp
+    obtain ⟨t, ht, rfl⟩ := Finset.mem_image.mp hp
+    exact (hMT t ht).trans (hL.2 t ht).symm
+  · rintro ⟨hM, hMa⟩
+    refine ⟨(latin_iff M).mpr hM, ?_⟩
+    intro t ht
+    exact (hMa _ (Finset.mem_image.mpr ⟨t, ht, rfl⟩)).trans (hL.2 t ht)
+
+theorem numCompletions_eq {n : ℕ} {T : Finset (Fin n × Fin n × Fin n)}
+    {L : Fin n → Fin n → Fin n} (hL : Completes T L) :
+    numCompletions T = (completions (T.image fun t => (t.1, t.2.1)) L).card := by
+  rw [numCompletions, ← Nat.card_eq_finsetCard]
+  exact Nat.card_congr (Equiv.subtypeEquivRight fun M =>
+    (completes_iff hL M).trans mem_completions.symm)
+
+theorem numCompletions_eq_one {n : ℕ} {L : Fin n → Fin n → Fin n}
+    {T : Finset (Fin n × Fin n × Fin n)} (h : DefiningSet L T) :
+    numCompletions T = 1 := by
+  rw [numCompletions, Nat.card_eq_one_iff_unique]
+  exact ⟨⟨fun a b => Subtype.ext ((h.2 a.1 a.2).trans (h.2 b.1 b.2).symm)⟩,
+    ⟨⟨L, h.1⟩⟩⟩
+
+/-! ## Theorem A -/
+
+/-- **Theorem A.** A set of fewer than `⌊n²/4⌋` filled cells has an even
+number of completions. -/
+theorem completions_even {n : ℕ} (T : Finset (Fin n × Fin n × Fin n))
+    (hT : T.card < n * n / 4) : Even (numCompletions T) := by
+  by_cases h : ∃ L, Completes T L
+  · obtain ⟨L, hL⟩ := h
+    rw [numCompletions_eq hL]
+    exact completions_card_even _ L ((latin_iff L).mp hL.1)
+      (lt_of_le_of_lt Finset.card_image_le hT)
+  · have : IsEmpty {L : Fin n → Fin n → Fin n // Completes T L} :=
+      ⟨fun L => h ⟨L.1, L.2⟩⟩
+    rw [numCompletions, Nat.card_of_isEmpty]
+    exact Even.zero
+
+/-- Since `1` is odd, Theorem A gives the lower bound: every defining set of
+every Latin square of order `n` has at least `⌊n²/4⌋` filled cells. -/
+theorem definingSet_card {n : ℕ} {L : Fin n → Fin n → Fin n}
+    {T : Finset (Fin n × Fin n × Fin n)} (h : DefiningSet L T) :
+    n * n / 4 ≤ T.card := by
+  by_contra hlt
+  have he := completions_even T (not_le.mp hlt)
+  rw [numCompletions_eq_one h] at he
+  exact Nat.not_even_one he
+
+/-! ## Theorem B -/
+
+/-- Emptying filled cells one at a time while the completion stays unique ends
+at a critical set. -/
+theorem exists_criticalSet_subset {n : ℕ} {L : Fin n → Fin n → Fin n} :
+    ∀ (k : ℕ) (T : Finset (Fin n × Fin n × Fin n)), T.card = k →
+      DefiningSet L T → ∃ T' ⊆ T, CriticalSet L T' := by
+  intro k
+  induction k using Nat.strong_induction_on with
+  | _ k ih =>
+    intro T hk hT
+    by_cases hc : ∀ t ∈ T, 1 < numCompletions (T.erase t)
+    · exact ⟨T, subset_refl T, hT, hc⟩
+    push Not at hc
+    obtain ⟨t, ht, hle⟩ := hc
+    have hLc : Completes (T.erase t) L :=
+      ⟨hT.1.1, fun u hu => hT.1.2 u (Finset.mem_of_mem_erase hu)⟩
+    rw [numCompletions] at hle
+    have hsub := (Finite.card_le_one_iff_subsingleton).mp hle
+    have hdef : DefiningSet L (T.erase t) :=
+      ⟨hLc, fun M hM => congrArg Subtype.val
+        (Subsingleton.elim (⟨M, hM⟩ : {M // Completes (T.erase t) M}) ⟨L, hLc⟩)⟩
+    obtain ⟨T', hsub', hcrit⟩ := ih (T.erase t).card
+      (hk ▸ Finset.card_erase_lt_of_mem ht) (T.erase t) rfl hdef
+    exact ⟨T', hsub'.trans (Finset.erase_subset t T), hcrit⟩
+
+/-- Every Latin square has a critical set: start from all `n²` filled cells. -/
+theorem exists_criticalSet {n : ℕ} {L : Fin n → Fin n → Fin n} (hL : Latin L) :
+    ∃ T, CriticalSet L T := by
+  let T := (Finset.univ : Finset (Fin n × Fin n)).image
+    (fun p => (p.1, p.2, L p.1 p.2))
+  have hT : DefiningSet L T := by
+    refine ⟨⟨hL, ?_⟩, ?_⟩
+    · intro t ht
+      obtain ⟨p, _, rfl⟩ := Finset.mem_image.mp ht
+      rfl
+    · intro M hM
+      funext r c
+      exact hM.2 (r, c, L r c) (Finset.mem_image.mpr ⟨(r, c), Finset.mem_univ _, rfl⟩)
+  obtain ⟨T', _, hT'⟩ := exists_criticalSet_subset T.card T rfl hT
+  exact ⟨T', hT'⟩
+
+theorem quarter_le_scsOf {n : ℕ} {L : Fin n → Fin n → Fin n} (hL : Latin L) :
+    n * n / 4 ≤ scsOf L := by
+  obtain ⟨T, hT⟩ := exists_criticalSet hL
+  unfold scsOf
+  exact le_csInf ⟨T.card, T, hT, rfl⟩ (by
+    rintro m ⟨T', hT', rfl⟩
+    exact definingSet_card hT'.1)
+
+/-- The two corner triangles of `B_n` form a critical set of size `⌊n²/4⌋`. -/
+theorem cyclic_criticalSet (n : ℕ) (hn : 0 < n) :
+    ∃ T, CriticalSet (cyclicSquare n) T ∧ T.card = n * n / 4 := by
+  let f : Fin n × Fin n → Fin n × Fin n × Fin n :=
+    fun p => (p.1, p.2, cyclicSquare n p.1 p.2)
+  have hf : Function.Injective f := by
+    intro p q h
+    simp only [f, Prod.mk.injEq] at h
+    exact Prod.ext h.1 h.2.1
+  let T := (cornerSet n).image f
+  have hcard : T.card = n * n / 4 := by
+    rw [Finset.card_image_of_injective _ hf, cornerSet_card n hn]
+  have hdef := cornerSet_isDefining n hn
+  have hlat : Latin (cyclicSquare n) := by
+    rw [latin_iff, cyclicSquare_eq]
+    exact hdef.1
+  have hcomp : Completes T (cyclicSquare n) := by
+    refine ⟨hlat, ?_⟩
+    intro t ht
+    obtain ⟨p, _, rfl⟩ := Finset.mem_image.mp ht
+    rfl
+  have hT : DefiningSet (cyclicSquare n) T := by
+    refine ⟨hcomp, ?_⟩
+    intro M hM
+    rw [cyclicSquare_eq]
+    apply hdef.2 M ((latin_iff M).mp hM.1)
+    intro p hp
+    have hMp : M p.1 p.2 = cyclicSquare n p.1 p.2 :=
+      hM.2 (f p) (Finset.mem_image.mpr ⟨p, hp, rfl⟩)
+    rw [hMp, cyclicSquare_eq]
+  refine ⟨T, ⟨hT, ?_⟩, hcard⟩
+  intro t ht
+  have hLc : Completes (T.erase t) (cyclicSquare n) :=
+    ⟨hlat, fun u hu => hcomp.2 u (Finset.mem_of_mem_erase hu)⟩
+  by_contra hle
+  rw [not_lt, numCompletions] at hle
+  have hsub := (Finite.card_le_one_iff_subsingleton).mp hle
+  have hdef' : DefiningSet (cyclicSquare n) (T.erase t) :=
+    ⟨hLc, fun M hM => congrArg Subtype.val
+      (Subsingleton.elim (⟨M, hM⟩ : {M // Completes (T.erase t) M}) ⟨_, hLc⟩)⟩
+  have h1 := definingSet_card hdef'
+  have h2 := Finset.card_erase_lt_of_mem ht
+  rw [hcard] at h2
+  exact (not_le.mpr h2) h1
+
+/-- **Theorem B.** For every `n ≥ 1`, `scs(n) = scs(B_n) = ⌊n²/4⌋`. -/
+theorem scs_eq_quarter (n : ℕ) (hn : 0 < n) :
+    scs n = n * n / 4 ∧ scsOf (cyclicSquare n) = n * n / 4 := by
+  obtain ⟨T, hT, hcard⟩ := cyclic_criticalSet n hn
+  have hlat : Latin (cyclicSquare n) := hT.1.1.1
+  have hcyc : scsOf (cyclicSquare n) = n * n / 4 := by
+    apply le_antisymm _ (quarter_le_scsOf hlat)
+    rw [← hcard]
+    unfold scsOf
+    exact Nat.sInf_le ⟨T, hT, rfl⟩
+  refine ⟨le_antisymm ?_ ?_, hcyc⟩
+  · rw [← hcyc]
+    unfold scs
+    exact Nat.sInf_le ⟨cyclicSquare n, hlat, rfl⟩
+  · unfold scs
+    exact le_csInf ⟨_, cyclicSquare n, hlat, rfl⟩ (by
+      rintro m ⟨L, hL, rfl⟩
+      exact quarter_le_scsOf hL)
+
+/-- A check of the definitions alone, at order 2: the empty set of filled cells
+has a second completion besides `B_2`, so it is not a defining set. -/
+example : ¬ DefiningSet (cyclicSquare 2) ∅ := by
+  rintro ⟨_, huniq⟩
+  have hM : Completes (∅ : Finset (Fin 2 × Fin 2 × Fin 2)) (fun r c => r + c + 1) :=
+    ⟨(latin_iff _).mpr (by unfold IsLatin; decide), by simp⟩
+  have h := congrFun (congrFun (huniq _ hM) 0) 0
+  revert h
+  decide
+
+end LatinQuarter.Textbook
diff --git a/LeanPool/LatinQuarter/Vanishing.lean b/LeanPool/LatinQuarter/Vanishing.lean
new file mode 100644
index 0000000000..024be41d9c
--- /dev/null
+++ b/LeanPool/LatinQuarter/Vanishing.lean
@@ -0,0 +1,98 @@
+/-
+Copyright (c) 2026 Richard Bean. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Bean
+-/
+module
+
+public import Mathlib.LinearAlgebra.Matrix.SchurComplement
+public import Mathlib.Algebra.CharP.Frobenius
+public import LeanPool.LatinQuarter.Minors
+public import LeanPool.LatinQuarter.SquareZero
+
+/-!
+# Vanishing of products of matrix minors
+-/
+
+@[expose] public section
+
+namespace LatinQuarter
+open scoped BigOperators Matrix
+
+variable {R : Type*} [CommRing R] [CharP R 2]
+
+/-- The square map is a ring homomorphism in characteristic two. -/
+noncomputable abbrev squareHom : R →+* R := frobenius R 2
+
+/-- Marked top-left block entries square to the identity, so that block
+is invertible even though the coefficient ring is not a field. -/
+theorem isUnit_det_of_square_map_eq_one {k : ℕ}
+    (A : Matrix (Fin k) (Fin k) R)
+    (hA : squareHom.mapMatrix A = 1) : IsUnit A.det := by
+  have hs : A.det * A.det = 1 := by
+    have hm := squareHom.map_det A
+    rw [hA, Matrix.det_one] at hm
+    simpa only [squareHom, frobenius_def, pow_two] using hm
+  exact ⟨⟨A.det, A.det, hs, hs⟩, rfl⟩
+
+/-- One block elimination gives a common ideal for all the minors. -/
+theorem marked_blocks_minor_ideal {k h : ℕ}
+    (A : Matrix (Fin k) (Fin k) R)
+    (B : Matrix (Fin k) (Fin h) R)
+    (C : Matrix (Fin h) (Fin k) R)
+    (D : Matrix (Fin h) (Fin h) R)
+    (hA : squareHom.mapMatrix A = 1)
+    (hC : C.map squareHom = 0)
+    (hD : D.map squareHom = 0) :
+    ∃ z : Fin h × Fin h → R,
+      (∀ j, z j * z j = 0) ∧
+      ∀ t, AllMinorsIn (Matrix.fromBlocks A B C D) t
+        (Ideal.span (Set.range z) ^ (t - k)) := by
+  classical
+  let := Matrix.invertibleOfIsUnitDet A (isUnit_det_of_square_map_eq_one A hA)
+  let Z := D - C * ⅟A * B
+  let z : Fin h × Fin h → R := fun p => Z p.1 p.2
+  refine ⟨z, ?_, ?_⟩
+  · have hm : squareHom.mapMatrix Z = 0 := by
+      simp only [Z, RingHom.mapMatrix_apply, Matrix.map_sub _ (map_sub squareHom),
+        Matrix.map_mul]
+      change D.map squareHom -
+        C.map squareHom * squareHom.mapMatrix (⅟A) * B.map squareHom = 0
+      rw [hC, hD, Matrix.zero_mul, Matrix.zero_mul, sub_zero]
+    intro j
+    have hj := congrArg (fun M => M j.1 j.2) hm
+    simpa only [RingHom.mapMatrix_apply, Matrix.map_apply, squareHom,
+      frobenius_def, pow_two, Matrix.zero_apply] using hj
+  · intro t
+    rw [Matrix.fromBlocks_eq_of_invertible₁₁ A B C D]
+    apply allMinorsIn_mul_right
+    apply allMinorsIn_mul_left
+    apply allMinorsIn_fromBlocks_diagonal
+    intro i j
+    exact Ideal.subset_span ⟨(i, j), rfl⟩
+
+/-- The abstract vanishing lemma: more residual factors than residual
+positions force a repeated square-zero entry. -/
+theorem marked_blocks_product_vanishes {k h : ℕ} {ι : Type*} [Fintype ι]
+    (A : Matrix (Fin k) (Fin k) R)
+    (B : Matrix (Fin k) (Fin h) R)
+    (C : Matrix (Fin h) (Fin k) R)
+    (D : Matrix (Fin h) (Fin h) R)
+    (hA : squareHom.mapMatrix A = 1)
+    (hC : C.map squareHom = 0)
+    (hD : D.map squareHom = 0)
+    (t : ι → ℕ)
+    (r c : (i : ι) → Fin (t i) → Fin k ⊕ Fin h)
+    (hbudget : h * h < ∑ i, (t i - k)) :
+    (∏ i, ((Matrix.fromBlocks A B C D).submatrix (r i) (c i)).det) = 0 := by
+  classical
+  obtain ⟨z, hz, hm⟩ := marked_blocks_minor_ideal A B C D hA hC hD
+  have hp := Ideal.prod_mem_prod (s := Finset.univ)
+    (I := fun i => Ideal.span (Set.range z) ^ (t i - k))
+    (x := fun i => ((Matrix.fromBlocks A B C D).submatrix (r i) (c i)).det)
+    (fun i _ => hm (t i) (r i) (c i))
+  rw [Finset.prod_pow_eq_pow_sum] at hp
+  rw [span_square_zero_pow_eq_bot z hz (by simpa using hbudget)] at hp
+  exact hp
+
+end LatinQuarter
diff --git a/LeanPool/projects/latin-quarter.yaml b/LeanPool/projects/latin-quarter.yaml
new file mode 100644
index 0000000000..c12256a8a2
--- /dev/null
+++ b/LeanPool/projects/latin-quarter.yaml
@@ -0,0 +1,50 @@
+slug: latin-quarter
+title: The smallest critical set in a Latin square
+summary: >-
+  Proves that every partial Latin square of order n with fewer than floor(n²/4)
+  filled cells has an even number of completions. Consequently every defining
+  set has at least floor(n²/4) entries, and the two corner triangles in the cyclic
+  square attain this bound as a critical set. Includes general results on matrix
+  minors, square-zero ideals, and square-free polynomial coefficients.
+branch: Combinatorics
+entry_module: LeanPool.LatinQuarter
+authors:
+  - Richard Bean
+source:
+  arxiv: '2610.18199'
+  url: https://github.com/RichardBean/latin-quarter-lean/tree/9997439dee62e1ede0aa995ddb7160dbceeff7b7
+  github_repo: RichardBean/latin-quarter-lean
+  commit: 9997439dee62e1ede0aa995ddb7160dbceeff7b7
+  announcement_url: https://github.com/RichardBean/latin-quarter-lean/releases/tag/v0.2.0
+  announcement_date: '2026-10-16'
+license: Apache-2.0
+status: verified
+provenance: AI
+main_declarations:
+  - LatinQuarter.Textbook.completions_even
+  - LatinQuarter.Textbook.scs_eq_quarter
+main_results:
+  - declaration: LatinQuarter.Textbook.completions_even
+    informal: >-
+      Every set of fewer than floor(n²/4) filled triples of an order-n partial
+      Latin square has an even number of labelled Latin-square completions.
+  - declaration: LatinQuarter.Textbook.scs_eq_quarter
+    informal: >-
+      For every positive n, the smallest critical-set size among all Latin
+      squares of order n, and the smallest critical-set size in the cyclic
+      Latin square, both equal floor(n²/4).
+  - declaration: LatinQuarter.defining_set_lower_bound
+    informal: >-
+      Every defining set in every labelled Latin square of order n has at least
+      floor(n²/4) cells.
+  - declaration: LatinQuarter.cornerSet_isCritical
+    informal: >-
+      For every positive n, the two opposite corner triangles form a critical
+      set in the cyclic Latin square.
+tags:
+  - combinatorics
+  - latin-squares
+  - critical-sets
+  - parity
+msc:
+  - 05B15