Conjectures about Latin Squares

This file formalizes some conjectures and theorems around latin squares.

References:

• [Wa2011] Wanless, Ian. "Transversals in Latin Squares: A Survey." Surveys in Combinatorics 2011, R. Chapman, Ed. Cambridge University Press, 2011, pp. 403–437. https://users.monash.edu.au/~iwanless/papers/transurveyBCC.pdf
• https://en.wikipedia.org/wiki/Problems_in_Latin_squares

theorem oddOrderLatinSquareTransversal {n : ℕ} : True ↔ Odd n → ∀ (L : LatinSquare n), ∃ (σ : Fin n → Fin n), IsTransversal L σ

Conjecture 3.2 in [Wa2011]: Each Latin square of odd order has at least one transversal.

theorem oddOrderLeq9LatinSquareTransversal : True ↔ ∀ n ≤ 9, Odd n → ∀ (L : LatinSquare n), ∃ (σ : Fin n → Fin n), IsTransversal L σ

The conjecture is known to be true for $n \leq 9$.

theorem latinSquareOrder11Transversal : True ↔ ∀ (L : LatinSquare 11), ∃ (σ : Fin 11 → Fin 11), IsTransversal L σ

The smallest odd number for which this conjecture is not known is 11.

theorem latinSquareNearTransversal {n : ℕ} : True ↔ ∀ (L : LatinSquare n), ∃ (ρ : Fin (n - 1) → Fin n) (σ : Fin (n - 1) → Fin n), IsNearTransversal L ρ σ

Conjecture 5.1 in [Wa2011]: Every latin square has a near-transversal

def z (n : ℕ) : ℕ

The number of transversals of the Cayley table of the cyclic group $\mathbb{Z}_n$

Equations

• z n = numTransversals { mat := Matrix.of fun (i j : Fin n) => i + j, row_injective := ⋯, col_injective := ⋯ }

theorem z_zero : z 0 = 1

The $0 \times 0$ Cayley table has exactly $1$ transversal (vacuously).

theorem z_odd_values : [z 1, z 3, z 5, z 7] = [1, 3, 15, 133]

The number of transversals of the Cayley table of $\mathbb{Z}_n$ for odd $n$ forms OEIS A006717, starting with $z(1) = 1, z(3) = 3, z(5) = 15, z(7) = 133$.

theorem z_even (n : ℕ) : z (2 * (n + 1)) = 0

The Cayley table of $\mathbb{Z}_n$ for positive even $n$ has no transversals.

theorem numTransversalsZn : True ↔ ∃ c₁ > 0, ∃ c₂ < 1, ∃ (_ : c₁ < c₂), ∀ n ≥ 3, Odd n → ↑(z n) ∈ Set.Icc (c₁ ^ n * ↑n.factorial) (c₂ ^ n * ↑n.factorial)

Conjecture 6.7 in [Wa2011]: There exist real constants $0 < c_1 < c_2 < 1$ such that $$ c_1^n n! \leq z_n \leq c_2^n n! $$ for all odd $n \geq 3$.

theorem growthRateZn : True ↔ Filter.Tendsto (fun (n : ℕ) => 1 / ↑n * Real.log (↑(z n) / ↑n.factorial)) Filter.atTop (nhds (-1))

Conjecture 6.9 in [Wa2011]: $$ \lim_{n \to \infty} \frac{1}{n} \log(z_n / n!) = -1 $$ It is not even known if this limit exists.

def T (n : ℕ) : ℕ

The maximum number of transversals over all latin squares of order n.

Equations

• T n = Finset.univ.sup fun (L : LatinSquare n) => numTransversals L

theorem maxTransversalsBound : have c := √((3 - √3) / 6) * Real.exp (√3 / 6); ∀ n ≥ 5, ↑(T n) ∈ Set.Icc (15 ^ (↑n / 5)) (c ^ n * √↑n * ↑n.factorial)

Theorem 7.2 in [Wa2011]: For all $n \geq 5$, $$ 15^{n/5} \leq T(n) \leq c^n \sqrt{n} \cdot n! $$ where $c = \sqrt{\frac{3 - \sqrt{3}}{6}} \cdot e^{\sqrt{3}/6}$