The cyclic Latin square and its corner set

def LatinQuarter.cyclic (n : ℕ) : Square n

The addition table of Fin n, used to attain the critical-set bound.

Equations

• LatinQuarter.cyclic n r c = r + c

theorem LatinQuarter.cyclic_isLatin (n : ℕ) (hn : 0 < n) : IsLatin (cyclic n)

def LatinQuarter.cornerSet (n : ℕ) : Finset (Cell n)

The two opposite triangular corners in the cyclic Latin square.

Equations

• LatinQuarter.cornerSet n = {p : LatinQuarter.Cell n | ↑p.1 + ↑p.2 < n / 2 ∨ n + n / 2 ≤ ↑p.1 + ↑p.2}

@[simp]

theorem LatinQuarter.mem_cornerSet {n : ℕ} (r c : Fin n) : (r, c) ∈ cornerSet n ↔ ↑r + ↑c < n / 2 ∨ n + n / 2 ≤ ↑r + ↑c

def LatinQuarter.fillingOrder {n : ℕ} (r c : Fin n) : ℕ

Rows are visited from top to bottom, and each row from right to left.

Equations

• LatinQuarter.fillingOrder r c = ↑r * n + (n - 1 - ↑c)

theorem LatinQuarter.fillingOrder_row {n : ℕ} (r i c d : Fin n) (hi : i < r) : fillingOrder i d < fillingOrder r c

theorem LatinQuarter.fillingOrder_column {n : ℕ} (r c j : Fin n) (hj : c < j) : fillingOrder r j < fillingOrder r c

theorem LatinQuarter.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 : Fin n), fillingOrder i j < fillingOrder r c → M i j = cyclic n i j) : M r c = cyclic n r c

Every non-corner cell is forced by the cells preceding it.

theorem LatinQuarter.cornerSet_isDefining (n : ℕ) (hn : 0 < n) : IsDefining (cornerSet n) (cyclic n)