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.

def LatinQuarter.IsCritical {n : ℕ} (P : Finset (Cell n)) (L : Square n) : Prop

A critical set is a defining set with no proper defining subset.

Equations

• LatinQuarter.IsCritical P L = (LatinQuarter.IsDefining P L ∧ ∀ Q ⊂ P, ¬LatinQuarter.IsDefining Q L)

theorem LatinQuarter.critical_set_lower_bound {n : ℕ} (P : Finset (Cell n)) (L : Square n) (h : IsCritical P L) : n * n / 4 ≤ P.card

theorem LatinQuarter.cornerSet_card (n : ℕ) (hn : 0 < n) : (cornerSet n).card = n * n / 4

theorem LatinQuarter.cornerSet_isCritical (n : ℕ) (hn : 0 < n) : IsCritical (cornerSet n) (cyclic n)

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

The smallest critical-set size among all labelled Latin squares of order n. This definition contains no bound or cyclic-square assumption.

Equations

• LatinQuarter.scs n = sInf {m : ℕ | ∃ (L : LatinQuarter.Square n) (P : Finset (LatinQuarter.Cell n)), LatinQuarter.IsCritical P L ∧ P.card = m}

noncomputable def LatinQuarter.scsOf {n : ℕ} (L : Square n) : ℕ

The smallest critical-set size in one specified square.

Equations

• LatinQuarter.scsOf L = sInf {m : ℕ | ∃ (P : Finset (LatinQuarter.Cell n)), LatinQuarter.IsCritical P L ∧ P.card = m}

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

Main theorem: the least size over all Latin squares is floor(n²/4).

theorem LatinQuarter.cyclic_scs_eq_quarter (n : ℕ) (hn : 0 < n) : scsOf (cyclic n) = n * n / 4

The cyclic Latin square attains the same least size.

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

A single statement giving the unrestricted lower bound and an explicit critical set attaining it in the cyclic square.