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.

def LatinQuarter.Textbook.Latin {n : ℕ} (L : Fin n → Fin n → Fin n) : Prop

Each symbol occurs exactly once in every row and exactly once in every column.

Equations

• LatinQuarter.Textbook.Latin L = ((∀ (r s : Fin n), ∃! c : Fin n, L r c = s) ∧ ∀ (c s : Fin n), ∃! r : Fin n, L r c = s)

def LatinQuarter.Textbook.Completes {n : ℕ} (T : Finset (Fin n × Fin n × Fin n)) (L : Fin n → Fin n → Fin n) : Prop

L is a completion of T: a Latin square that agrees with every filled cell (row, column, symbol) of T.

Equations

• LatinQuarter.Textbook.Completes T L = (LatinQuarter.Textbook.Latin L ∧ ∀ t ∈ T, L t.1 t.2.1 = t.2.2)

noncomputable def LatinQuarter.Textbook.numCompletions {n : ℕ} (T : Finset (Fin n × Fin n × Fin n)) : ℕ

The number of completions of T, written N(P) in the paper.

Equations

• LatinQuarter.Textbook.numCompletions T = Nat.card { L : Fin n → Fin n → Fin n // LatinQuarter.Textbook.Completes T L }

def LatinQuarter.Textbook.DefiningSet {n : ℕ} (L : Fin n → Fin n → Fin n) (T : Finset (Fin n × Fin n × Fin n)) : Prop

T is a defining set of L: L is a completion of T, and the only one.

Equations

• LatinQuarter.Textbook.DefiningSet L T = (LatinQuarter.Textbook.Completes T L ∧ ∀ (M : Fin n → Fin n → Fin n), LatinQuarter.Textbook.Completes T M → M = L)

def LatinQuarter.Textbook.CriticalSet {n : ℕ} (L : Fin n → Fin n → Fin n) (T : Finset (Fin n × Fin n × Fin n)) : Prop

A defining set of L is critical if emptying any one of its filled cells leaves more than one completion.

Equations

• LatinQuarter.Textbook.CriticalSet L T = (LatinQuarter.Textbook.DefiningSet L T ∧ ∀ t ∈ T, 1 < LatinQuarter.Textbook.numCompletions (T.erase t))

noncomputable def LatinQuarter.Textbook.scsOf {n : ℕ} (L : Fin n → Fin n → Fin n) : ℕ

scs(L): the smallest number of filled cells in a critical set of L.

Equations

• LatinQuarter.Textbook.scsOf L = sInf {m : ℕ | ∃ (T : Finset (Fin n × Fin n × Fin n)), LatinQuarter.Textbook.CriticalSet L T ∧ T.card = m}

noncomputable def LatinQuarter.Textbook.scs (n : ℕ) : ℕ

scs(n): the minimum of scs(L) over all Latin squares L of order n.

Equations

• LatinQuarter.Textbook.scs n = sInf {m : ℕ | ∃ (L : Fin n → Fin n → Fin n), LatinQuarter.Textbook.Latin L ∧ LatinQuarter.Textbook.scsOf L = m}

def LatinQuarter.Textbook.cyclicSquare (n : ℕ) : Fin n → Fin n → Fin n

The cyclic square B_n, whose entry in cell (r, c) is (r + c) mod n.

Equations

• LatinQuarter.Textbook.cyclicSquare n r c = ⟨(↑r + ↑c) % n, ⋯⟩

Agreement with the package's definitions

theorem LatinQuarter.Textbook.latin_iff {n : ℕ} (L : Fin n → Fin n → Fin n) : Latin L ↔ IsLatin L

theorem LatinQuarter.Textbook.cyclicSquare_eq (n : ℕ) : cyclicSquare n = cyclic n

theorem LatinQuarter.Textbook.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 (Finset.image (fun (t : Fin n × Fin n × Fin n) => (t.1, t.2.1)) T) L M

Once L completes T, the completions of T are the Latin squares that agree with L on the cells of T.

theorem LatinQuarter.Textbook.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 (Finset.image (fun (t : Fin n × Fin n × Fin n) => (t.1, t.2.1)) T) L).card

theorem LatinQuarter.Textbook.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

Theorem A

theorem LatinQuarter.Textbook.completions_even {n : ℕ} (T : Finset (Fin n × Fin n × Fin n)) (hT : T.card < n * n / 4) : Even (numCompletions T)

Theorem A. A set of fewer than ⌊n²/4⌋ filled cells has an even number of completions.

theorem LatinQuarter.Textbook.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

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 B

theorem LatinQuarter.Textbook.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'

Emptying filled cells one at a time while the completion stays unique ends at a critical set.

theorem LatinQuarter.Textbook.exists_criticalSet {n : ℕ} {L : Fin n → Fin n → Fin n} (hL : Latin L) : ∃ (T : Finset (Fin n × Fin n × Fin n)), CriticalSet L T

Every Latin square has a critical set: start from all n² filled cells.

theorem LatinQuarter.Textbook.quarter_le_scsOf {n : ℕ} {L : Fin n → Fin n → Fin n} (hL : Latin L) : n * n / 4 ≤ scsOf L

theorem LatinQuarter.Textbook.cyclic_criticalSet (n : ℕ) (hn : 0 < n) : ∃ (T : Finset (Fin n × Fin n × Fin n)), CriticalSet (cyclicSquare n) T ∧ T.card = n * n / 4

The two corner triangles of B_n form a critical set of size ⌊n²/4⌋.

theorem LatinQuarter.Textbook.scs_eq_quarter (n : ℕ) (hn : 0 < n) : scs n = n * n / 4 ∧ scsOf (cyclicSquare n) = n * n / 4

Theorem B. For every n ≥ 1, scs(n) = scs(B_n) = ⌊n²/4⌋.