Import the sharp critical-set bound for Latin squares

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

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

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

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

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