FormalConjectures.Paper.LatinSquare

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

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


namespace LatinSquare


variable {n : ℕ}

Two latin squares of the same order are orthogonal if superimposing them gives each ordered pair of symbols at most once.

def Orthogonal (L M : LatinSquare n) : Prop :=
  Function.Injective fun p : Fin n × Fin n => (L.mat p.1 p.2, M.mat p.1 p.2)

A family of latin squares is mutually orthogonal if any two distinct members are orthogonal.

def MutuallyOrthogonal {k n : ℕ} (L : Fin k → LatinSquare n) : Prop :=
  ∀ ⦃i j : Fin k⦄, i ≠ j → Orthogonal (L i) (L j)

A complete set of mutually orthogonal latin squares (MOLS) of order n consists of n - 1 latin squares of order n, pairwise orthogonal to each other.

def HasCompleteMOLS (n : ℕ) : Prop :=
  0 < n ∧ ∃ L : Fin (n - 1) → LatinSquare n, MutuallyOrthogonal L

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

@[category research open, AMS 5]
theorem declaration uses 'sorry'oddOrderLatinSquareTransversal : answer(sorry) ↔
    Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ := byn:ℕ⊢ True ↔ Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ
  sorryAll goals completed! 🐙

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

@[category research solved, AMS 5]
theorem declaration uses 'sorry'oddOrderLeq9LatinSquareTransversal : answer(sorry) ↔
    ∀ n ≤ 9, Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ := by⊢ True ↔ ∀ n ≤ 9, Odd n → ∀ (L : LatinSquare n), ∃ σ, IsTransversal L σ
  sorryAll goals completed! 🐙

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

@[category research open, AMS 5]
theorem declaration uses 'sorry'latinSquareOrder11Transversal : answer(sorry) ↔
    ∀ (L : LatinSquare 11), ∃ σ, IsTransversal L σ := by⊢ True ↔ ∀ (L : LatinSquare 11), ∃ σ, IsTransversal L σ
  sorryAll goals completed! 🐙

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

@[category research open, AMS 5]
theorem declaration uses 'sorry'latinSquareNearTransversal : answer(sorry) ↔
    ∀ (L : LatinSquare n), ∃ ρ σ, IsNearTransversal L ρ σ := byn:ℕ⊢ True ↔ ∀ (L : LatinSquare n), ∃ ρ σ, IsNearTransversal L ρ σ
  sorryAll goals completed! 🐙

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

def z (n : ℕ) : ℕ := numTransversals {
  mat := Matrix.of fun i j : Fin n => i + j
  row_injective := fun i _a _b h => byn✝:ℕn:ℕi:Fin n_a:Fin n_b:Fin nh:Matrix.of (fun i j => i + j) i _a = Matrix.of (fun i j => i + j) i _b⊢ _a = _b
    simp only [Matrix.of_apply] at hn✝:ℕn:ℕi:Fin n_a:Fin n_b:Fin nh:i + _a = i + _b⊢ _a = _b; exact add_left_cancel hAll goals completed! 🐙
  col_injective := fun j _a _b h => byn✝:ℕn:ℕj:Fin n_a:Fin n_b:Fin nh:(Matrix.of fun i j => i + j).transpose j _a = (Matrix.of fun i j => i + j).transpose j _b⊢ _a = _b
    simp only [Matrix.transpose_apply, Matrix.of_apply] at hn✝:ℕn:ℕj:Fin n_a:Fin n_b:Fin nh:_a + j = _b + j⊢ _a = _b; exact add_right_cancel hAll goals completed! 🐙
}

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

@[category test, AMS 5]
theorem z_zero : z 0 = 1 := by⊢ z 0 = 1 native_decideAll goals completed! 🐙

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$.

@[category test, AMS 5]
theorem z_odd_values : [z 1, z 3, z 5, z 7] = [1, 3, 15, 133] := by⊢ [z 1, z 3, z 5, z 7] = [1, 3, 15, 133] native_decideAll goals completed! 🐙

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

@[category textbook, AMS 5]
theorem z_even (n : ℕ) : z (2 * (n + 1)) = 0 := byn:ℕ⊢ z (2 * (n + 1)) = 0
  set N := 2 * (n + 1) with hN_defn:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rfl⊢ z N = 0
  have hNpos : 0 < N := byn:ℕ⊢ z (2 * (n + 1)) = 0 positivityAll goals completed! 🐙
  haveI : NeZero N := ⟨hNpos.ne'⟩n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }⊢ z N = 0
  rw [z, numTransversals, Fintype.card_eq_zero_iff]n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }⊢ IsEmpty { σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }
  refine ⟨fun ⟨σ, hσ, himg⟩ => ?_⟩n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ }.mat i (σ i)⊢ False
  simp only [Matrix.of_apply] at himgn:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ i⊢ False
  let σE : Fin N ≃ Fin N := Equiv.ofBijective σ
    ((Fintype.bijective_iff_injective_and_card _).mpr ⟨hσ, rfl⟩)n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯⊢ False
  let fE : Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i)
    ((Fintype.bijective_iff_injective_and_card _).mpr ⟨himg, rfl⟩)n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯⊢ False
  -- Sum the cell labels in `ZMod N` via `Nat.cast ∘ Fin.val`.
  let g : Fin N → ZMod N := fun i => ((i : ℕ) : ZMod N)n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑i⊢ False
  set S : ZMod N := ∑ i : Fin N, g i with hS_defn:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rfl⊢ False
  have hcast : ∀ i : Fin N, g (i + σ i) = g i + g (σ i) := byn:ℕ⊢ z (2 * (n + 1)) = 0
    intro in:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rfli:Fin N⊢ g (i + σ i) = g i + g (σ i); simp only [g, Fin.val_add, ZMod.natCast_mod, Nat.cast_add]All goals completed! 🐙
  have h1 : (∑ i : Fin N, g (i + σ i)) = S := Equiv.sum_comp fE gn:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rflhcast:∀ (i : Fin N), g (i + σ i) = g i + g (σ i) := 
  fun i =>
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = ↑↑i + ↑↑(σ i)) (Eq.trans (ZMod.natCast_mod (↑i + ↑(σ i)) N) (Nat.cast_add ↑i ↑(σ i))))
        (eq_self (↑↑i + ↑↑(σ i))))h1:∑ i, g (i + σ i) = S := Equiv.sum_comp fE g⊢ False
  have h2 : (∑ i : Fin N, g (σ i)) = S := Equiv.sum_comp σE gn:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rflhcast:∀ (i : Fin N), g (i + σ i) = g i + g (σ i) := 
  fun i =>
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = ↑↑i + ↑↑(σ i)) (Eq.trans (ZMod.natCast_mod (↑i + ↑(σ i)) N) (Nat.cast_add ↑i ↑(σ i))))
        (eq_self (↑↑i + ↑↑(σ i))))h1:∑ i, g (i + σ i) = S := Equiv.sum_comp fE gh2:∑ i, g (σ i) = S := Equiv.sum_comp σE g⊢ False
  have hSS : S + S = S := byn:ℕ⊢ z (2 * (n + 1)) = 0
    calc S + S = (∑ i, g i) + ∑ i, g (σ i) := byn:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rflhcast:∀ (i : Fin N), g (i + σ i) = g i + g (σ i) := 
  fun i =>
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = ↑↑i + ↑↑(σ i)) (Eq.trans (ZMod.natCast_mod (↑i + ↑(σ i)) N) (Nat.cast_add ↑i ↑(σ i))))
        (eq_self (↑↑i + ↑↑(σ i))))h1:∑ i, g (i + σ i) = S := Equiv.sum_comp fE gh2:∑ i, g (σ i) = S := Equiv.sum_comp σE g⊢ S + S = ∑ i, g i + ∑ i, g (σ i) rw [h2]All goals completed! 🐙
      _ = ∑ i, (g i + g (σ i)) := (Finset.sum_add_distrib).symm
      _ = ∑ i, g (i + σ i) := byn:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rflhcast:∀ (i : Fin N), g (i + σ i) = g i + g (σ i) := 
  fun i =>
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = ↑↑i + ↑↑(σ i)) (Eq.trans (ZMod.natCast_mod (↑i + ↑(σ i)) N) (Nat.cast_add ↑i ↑(σ i))))
        (eq_self (↑↑i + ↑↑(σ i))))h1:∑ i, g (i + σ i) = S := Equiv.sum_comp fE gh2:∑ i, g (σ i) = S := Equiv.sum_comp σE g⊢ ∑ i, (g i + g (σ i)) = ∑ i, g (i + σ i) simp_rw [n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rflhcast:∀ (i : Fin N), g (i + σ i) = g i + g (σ i) := 
  fun i =>
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = ↑↑i + ↑↑(σ i)) (Eq.trans (ZMod.natCast_mod (↑i + ↑(σ i)) N) (Nat.cast_add ↑i ↑(σ i))))
        (eq_self (↑↑i + ↑↑(σ i))))h1:∑ i, g (i + σ i) = S := Equiv.sum_comp fE gh2:∑ i, g (σ i) = S := Equiv.sum_comp σE g⊢ ∑ i, (g i + g (σ i)) = ∑ i, g (i + σ i)← hcast]
      _ = S := h1
  have hS0 : S = 0 := byn:ℕ⊢ z (2 * (n + 1)) = 0 linear_combination hSSAll goals completed! 🐙
  -- `S = ∑_{i < N} i = N(N-1)/2 = (n+1)(2n+1)` in `ZMod N`.
  have hval : S = (((Finset.range N).sum id : ℕ) : ZMod N) := byn:ℕ⊢ z (2 * (n + 1)) = 0
    rw [hS_def]n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rflhcast:∀ (i : Fin N), g (i + σ i) = g i + g (σ i) := 
  fun i =>
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = ↑↑i + ↑↑(σ i)) (Eq.trans (ZMod.natCast_mod (↑i + ↑(σ i)) N) (Nat.cast_add ↑i ↑(σ i))))
        (eq_self (↑↑i + ↑↑(σ i))))h1:∑ i, g (i + σ i) = S := Equiv.sum_comp fE gh2:∑ i, g (σ i) = S := Equiv.sum_comp σE ghSS:S + S = S := 
  Trans.trans
    (Trans.trans
      (Trans.trans (Eq.mpr (id (congrArg (fun _a => S + S = ∑ i, g i + _a) h2)) (Eq.refl (S + S)))
        (Eq.symm Finset.sum_add_distrib))
      (of_eq_true
        (Eq.trans
          (congrArg (fun x => x = ∑ x, g (x + σ x))
            (Finset.sum_congr (Eq.refl Finset.univ) fun x a => (fun i => Eq.symm (hcast i)) x))
          (eq_self (∑ x, g (x + σ x))))))
    h1hS0:S = 0 := 
  Mathlib.Tactic.LinearCombination.eq_of_eq hSS
    (Mathlib.Tactic.LinearCombination.eq_rearrange
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.sub_congr
          (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf S) (Mathlib.Tactic.Ring.atom_pf S)
            (Mathlib.Tactic.Ring.add_pf_add_overlap
              (Mathlib.Tactic.Ring.add_overlap_pf S (Nat.rawCast 1)
                (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                  (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw (ZMod N) 1)
                    (Mathlib.Meta.NormNum.IsNat.of_raw (ZMod N) 1) (Eq.refl 2))))
              (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
          (Mathlib.Tactic.Ring.add_congr
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat (ZMod N) Nat.cast_zero))
            (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf S) (Mathlib.Tactic.Ring.atom_pf S)
              (Mathlib.Tactic.Ring.add_pf_add_overlap
                (Mathlib.Tactic.Ring.add_overlap_pf S (Nat.rawCast 1)
                  (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                    (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw (ZMod N) 1)
                      (Mathlib.Meta.NormNum.IsNat.of_raw (ZMod N) 1) (Eq.refl 2))))
                (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
            (Mathlib.Tactic.Ring.add_pf_zero_add (S ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))
          (Mathlib.Tactic.Ring.sub_pf
            (Mathlib.Tactic.Ring.neg_add
              (Mathlib.Tactic.Ring.neg_mul S (Nat.rawCast 1)
                (Mathlib.Tactic.Ring.neg_one_mul
                  (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                    (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                      (Mathlib.Meta.NormNum.IsInt.of_raw (ZMod N) (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw (ZMod N) 2))
                      (Eq.refl (Int.negOfNat 2))))))
              Mathlib.Tactic.Ring.neg_zero)
            (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
              (Mathlib.Tactic.Ring.add_overlap_pf_zero S (Nat.rawCast 1)
                (Mathlib.Meta.NormNum.IsInt.to_isNat
                  (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                    (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw (ZMod N) 2))
                    (Mathlib.Meta.NormNum.IsInt.of_raw (ZMod N) (Int.negOfNat 2)) (Eq.refl (Int.ofNat 0)))))
              (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
        (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat (ZMod N) Nat.cast_zero))))⊢ ∑ i, g i = ↑((Finset.range N).sum id)
    push_cast [g, Fin.sum_univ_eq_sum_range fun k => ((k : ℕ) : ZMod N), id]n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rflhcast:∀ (i : Fin N), g (i + σ i) = g i + g (σ i) := 
  fun i =>
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = ↑↑i + ↑↑(σ i)) (Eq.trans (ZMod.natCast_mod (↑i + ↑(σ i)) N) (Nat.cast_add ↑i ↑(σ i))))
        (eq_self (↑↑i + ↑↑(σ i))))h1:∑ i, g (i + σ i) = S := Equiv.sum_comp fE gh2:∑ i, g (σ i) = S := Equiv.sum_comp σE ghSS:S + S = S := 
  Trans.trans
    (Trans.trans
      (Trans.trans (Eq.mpr (id (congrArg (fun _a => S + S = ∑ i, g i + _a) h2)) (Eq.refl (S + S)))
        (Eq.symm Finset.sum_add_distrib))
      (of_eq_true
        (Eq.trans
          (congrArg (fun x => x = ∑ x, g (x + σ x))
            (Finset.sum_congr (Eq.refl Finset.univ) fun x a => (fun i => Eq.symm (hcast i)) x))
          (eq_self (∑ x, g (x + σ x))))))
    h1hS0:S = 0 := 
  Mathlib.Tactic.LinearCombination.eq_of_eq hSS
    (Mathlib.Tactic.LinearCombination.eq_rearrange
      (Mathlib.Tactic.Ring.of_eq
        (Mathlib.Tactic.Ring.sub_congr
          (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf S) (Mathlib.Tactic.Ring.atom_pf S)
            (Mathlib.Tactic.Ring.add_pf_add_overlap
              (Mathlib.Tactic.Ring.add_overlap_pf S (Nat.rawCast 1)
                (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                  (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw (ZMod N) 1)
                    (Mathlib.Meta.NormNum.IsNat.of_raw (ZMod N) 1) (Eq.refl 2))))
              (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
          (Mathlib.Tactic.Ring.add_congr
            (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat (ZMod N) Nat.cast_zero))
            (Mathlib.Tactic.Ring.add_congr (Mathlib.Tactic.Ring.atom_pf S) (Mathlib.Tactic.Ring.atom_pf S)
              (Mathlib.Tactic.Ring.add_pf_add_overlap
                (Mathlib.Tactic.Ring.add_overlap_pf S (Nat.rawCast 1)
                  (Mathlib.Meta.NormNum.IsNat.to_raw_eq
                    (Mathlib.Meta.NormNum.isNat_add (Eq.refl HAdd.hAdd) (Mathlib.Meta.NormNum.IsNat.of_raw (ZMod N) 1)
                      (Mathlib.Meta.NormNum.IsNat.of_raw (ZMod N) 1) (Eq.refl 2))))
                (Mathlib.Tactic.Ring.add_pf_zero_add 0)))
            (Mathlib.Tactic.Ring.add_pf_zero_add (S ^ Nat.rawCast 1 * Nat.rawCast 2 + 0)))
          (Mathlib.Tactic.Ring.sub_pf
            (Mathlib.Tactic.Ring.neg_add
              (Mathlib.Tactic.Ring.neg_mul S (Nat.rawCast 1)
                (Mathlib.Tactic.Ring.neg_one_mul
                  (Mathlib.Meta.NormNum.IsInt.to_raw_eq
                    (Mathlib.Meta.NormNum.isInt_mul (Eq.refl HMul.hMul)
                      (Mathlib.Meta.NormNum.IsInt.of_raw (ZMod N) (Int.negOfNat 1))
                      (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw (ZMod N) 2))
                      (Eq.refl (Int.negOfNat 2))))))
              Mathlib.Tactic.Ring.neg_zero)
            (Mathlib.Tactic.Ring.add_pf_add_overlap_zero
              (Mathlib.Tactic.Ring.add_overlap_pf_zero S (Nat.rawCast 1)
                (Mathlib.Meta.NormNum.IsInt.to_isNat
                  (Mathlib.Meta.NormNum.isInt_add (Eq.refl HAdd.hAdd)
                    (Mathlib.Meta.NormNum.IsNat.to_isInt (Mathlib.Meta.NormNum.IsNat.of_raw (ZMod N) 2))
                    (Mathlib.Meta.NormNum.IsInt.of_raw (ZMod N) (Int.negOfNat 2)) (Eq.refl (Int.ofNat 0)))))
              (Mathlib.Tactic.Ring.add_pf_zero_add 0))))
        (Mathlib.Tactic.Ring.cast_zero (Mathlib.Meta.NormNum.isNat_ofNat (ZMod N) Nat.cast_zero))))⊢ ∑ i ∈ Finset.range N, ↑i = ∑ x ∈ Finset.range N, ↑x
    rflAll goals completed! 🐙
  rw [hval, show (Finset.range N).sum id = ∑ i ∈ Finset.range N, i from rfl,
    Finset.sum_range_id] at hS0n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rflhcast:∀ (i : Fin N), g (i + σ i) = g i + g (σ i) := 
  fun i =>
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = ↑↑i + ↑↑(σ i)) (Eq.trans (ZMod.natCast_mod (↑i + ↑(σ i)) N) (Nat.cast_add ↑i ↑(σ i))))
        (eq_self (↑↑i + ↑↑(σ i))))h1:∑ i, g (i + σ i) = S := Equiv.sum_comp fE gh2:∑ i, g (σ i) = S := Equiv.sum_comp σE ghSS:S + S = S := 
  Trans.trans
    (Trans.trans
      (Trans.trans (Eq.mpr (id (congrArg (fun _a => S + S = ∑ i, g i + _a) h2)) (Eq.refl (S + S)))
        (Eq.symm Finset.sum_add_distrib))
      (of_eq_true
        (Eq.trans
          (congrArg (fun x => x = ∑ x, g (x + σ x))
            (Finset.sum_congr (Eq.refl Finset.univ) fun x a => (fun i => Eq.symm (hcast i)) x))
          (eq_self (∑ x, g (x + σ x))))))
    h1hS0:↑(N * (N - 1) / 2) = 0hval:S = ↑((Finset.range N).sum id)⊢ False
  have hdiv : N * (N - 1) / 2 = (n + 1) * (2 * n + 1) := byn:ℕ⊢ z (2 * (n + 1)) = 0
    rw [hN_def, show 2 * (n + 1) - 1 = 2 * n + 1 from by omega,
      show 2 * (n + 1) * (2 * n + 1) = 2 * ((n + 1) * (2 * n + 1)) from by ring,
      Nat.mul_div_cancel_left _ (by norm_num : 0 < 2)]All goals completed! 🐙
  rw [hdiv] at hS0n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rflhcast:∀ (i : Fin N), g (i + σ i) = g i + g (σ i) := 
  fun i =>
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = ↑↑i + ↑↑(σ i)) (Eq.trans (ZMod.natCast_mod (↑i + ↑(σ i)) N) (Nat.cast_add ↑i ↑(σ i))))
        (eq_self (↑↑i + ↑↑(σ i))))h1:∑ i, g (i + σ i) = S := Equiv.sum_comp fE gh2:∑ i, g (σ i) = S := Equiv.sum_comp σE ghSS:S + S = S := 
  Trans.trans
    (Trans.trans
      (Trans.trans (Eq.mpr (id (congrArg (fun _a => S + S = ∑ i, g i + _a) h2)) (Eq.refl (S + S)))
        (Eq.symm Finset.sum_add_distrib))
      (of_eq_true
        (Eq.trans
          (congrArg (fun x => x = ∑ x, g (x + σ x))
            (Finset.sum_congr (Eq.refl Finset.univ) fun x a => (fun i => Eq.symm (hcast i)) x))
          (eq_self (∑ x, g (x + σ x))))))
    h1hS0:↑((n + 1) * (2 * n + 1)) = 0hval:S = ↑((Finset.range N).sum id)hdiv:N * (N - 1) / 2 = (n + 1) * (2 * n + 1)⊢ False
  have hdvd : N ∣ (n + 1) * (2 * n + 1) := (ZMod.natCast_eq_zero_iff _ _).mp hS0n:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rflhcast:∀ (i : Fin N), g (i + σ i) = g i + g (σ i) := 
  fun i =>
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = ↑↑i + ↑↑(σ i)) (Eq.trans (ZMod.natCast_mod (↑i + ↑(σ i)) N) (Nat.cast_add ↑i ↑(σ i))))
        (eq_self (↑↑i + ↑↑(σ i))))h1:∑ i, g (i + σ i) = S := Equiv.sum_comp fE gh2:∑ i, g (σ i) = S := Equiv.sum_comp σE ghSS:S + S = S := 
  Trans.trans
    (Trans.trans
      (Trans.trans (Eq.mpr (id (congrArg (fun _a => S + S = ∑ i, g i + _a) h2)) (Eq.refl (S + S)))
        (Eq.symm Finset.sum_add_distrib))
      (of_eq_true
        (Eq.trans
          (congrArg (fun x => x = ∑ x, g (x + σ x))
            (Finset.sum_congr (Eq.refl Finset.univ) fun x a => (fun i => Eq.symm (hcast i)) x))
          (eq_self (∑ x, g (x + σ x))))))
    h1hS0:↑((n + 1) * (2 * n + 1)) = 0hval:S = ↑((Finset.range N).sum id)hdiv:N * (N - 1) / 2 = (n + 1) * (2 * n + 1)hdvd:N ∣ (n + 1) * (2 * n + 1) := (ZMod.natCast_eq_zero_iff ((n + 1) * (2 * n + 1)) N).mp hS0⊢ False
  -- `N = (n+1) * 2`; cancelling `(n+1)` forces `2 ∣ 2n+1`, impossible.
  rw [hN_def, show 2 * (n + 1) = (n + 1) * 2 from by ring,
    mul_dvd_mul_iff_left (Nat.succ_ne_zero n)] at hdvdn:ℕN:ℕ := 2 * (n + 1)hN_def:N = 2 * (n + 1) := rflhNpos:0 < N := 
  mul_pos (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 2)) (Eq.refl (Nat.ble 1 2)))
    (Right.add_pos_of_nonneg_of_pos (zero_le n)
      (Mathlib.Meta.Positivity.pos_of_isNat (Mathlib.Meta.NormNum.isNat_ofNat ℕ (Eq.refl 1)) (Eq.refl (Nat.ble 1 1))))this:NeZero N := { out := LT.lt.ne' hNpos }x✝:{ σ // IsTransversal { mat := Matrix.of fun i j => i + j, row_injective := ⋯, col_injective := ⋯ } σ }σ:Fin N → Fin Nhσ:Function.Injective σhimg:Function.Injective fun i => i + σ iσE:Fin N ≃ Fin N := Equiv.ofBijective σ ⋯fE:Fin N ≃ Fin N := Equiv.ofBijective (fun i => i + σ i) ⋯g:Fin N → ZMod N := fun i => ↑↑iS:ZMod N := ∑ i, g ihS_def:S = ∑ i, g i := rflhcast:∀ (i : Fin N), g (i + σ i) = g i + g (σ i) := 
  fun i =>
    of_eq_true
      (Eq.trans
        (congrArg (fun x => x = ↑↑i + ↑↑(σ i)) (Eq.trans (ZMod.natCast_mod (↑i + ↑(σ i)) N) (Nat.cast_add ↑i ↑(σ i))))
        (eq_self (↑↑i + ↑↑(σ i))))h1:∑ i, g (i + σ i) = S := Equiv.sum_comp fE gh2:∑ i, g (σ i) = S := Equiv.sum_comp σE ghSS:S + S = S := 
  Trans.trans
    (Trans.trans
      (Trans.trans (Eq.mpr (id (congrArg (fun _a => S + S = ∑ i, g i + _a) h2)) (Eq.refl (S + S)))
        (Eq.symm Finset.sum_add_distrib))
      (of_eq_true
        (Eq.trans
          (congrArg (fun x => x = ∑ x, g (x + σ x))
            (Finset.sum_congr (Eq.refl Finset.univ) fun x a => (fun i => Eq.symm (hcast i)) x))
          (eq_self (∑ x, g (x + σ x))))))
    h1hS0:↑((n + 1) * (2 * n + 1)) = 0hval:S = ↑((Finset.range N).sum id)hdiv:N * (N - 1) / 2 = (n + 1) * (2 * n + 1)hdvd:2 ∣ 2 * n + 1⊢ False
  omegaAll goals completed! 🐙

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$.

@[category research open, AMS 5]
theorem declaration uses 'sorry'numTransversalsZn : answer(sorry) ↔
      ∃ᵉ (c₁ > (0 : ℝ)) (c₂ < (1 : ℝ)) (_ : c₁ < c₂),
      ∀ n ≥ 3, Odd n →
        (z n : ℝ) ∈ Set.Icc (c₁ ^ n * n.factorial) (c₂ ^ n * n.factorial) := by⊢ True ↔
  ∃ c₁ > 0, ∃ c₂ < 1, ∃ (_ : c₁ < c₂), ∀ n ≥ 3, Odd n → ↑(z n) ∈ Set.Icc (c₁ ^ n * ↑n.factorial) (c₂ ^ n * ↑n.factorial)
  sorryAll goals completed! 🐙

Conjecture 6.9 in [Wa2011]: $$ \lim_{\substack{n \to \infty \ n \text{ odd}}} \frac{1}{n} \log(z_n / n!) = -1 $$ It is not even known if this limit exists. Note that $z_n = 0$ for even $n$ (see z_even), so the limit must be restricted to odd $n$; here we parametrise odd $n$ as $2k + 1$.

@[category research open, AMS 5]
theorem declaration uses 'sorry'growthRateZn : answer(sorry) ↔
    Filter.Tendsto (fun k => (1 : ℝ) / (2 * k + 1) *
      Real.log (z (2 * k + 1) / (2 * k + 1).factorial)) Filter.atTop
      (nhds (-1)) := by⊢ True ↔
  Filter.Tendsto (fun k => 1 / (2 * ↑k + 1) * Real.log (↑(z (2 * k + 1)) / ↑(2 * k + 1).factorial)) Filter.atTop
    (nhds (-1))
  sorryAll goals completed! 🐙

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

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

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}$

@[category research solved, AMS 5]
theorem declaration uses 'sorry'maxTransversalsBound :
    let c := Real.sqrt ((3 - Real.sqrt 3) / 6) * Real.exp (Real.sqrt 3 / 6)
    ∀ n : ℕ, n ≥ 5 →
      (T n : ℝ) ∈ Set.Icc ((15 : ℝ) ^ ((n : ℝ) / 5)) (c ^ n * Real.sqrt n * n.factorial) := by⊢ let c := √((3 - √3) / 6) * Real.exp (√3 / 6);
∀ n ≥ 5, ↑(T n) ∈ Set.Icc (15 ^ (↑n / 5)) (c ^ n * √↑n * ↑n.factorial)
  sorryAll goals completed! 🐙

MOLS existence problem: determine exactly which orders n admit a complete set of n - 1 mutually orthogonal latin squares.

Equivalently, this asks for which orders affine planes of order n exist. Complete sets are known for prime-power orders; the smallest currently unresolved order is 12.

@[category research open, AMS 5]
theorem declaration uses 'sorry'molsExistenceProblem : answer(sorry) = {n : ℕ | HasCompleteMOLS n} := by⊢ sorry = {n | HasCompleteMOLS n}
  sorryAll goals completed! 🐙

The smallest unresolved case of the MOLS existence problem: whether there are 11 mutually orthogonal latin squares of order 12.

@[category research open, AMS 5]
theorem declaration uses 'sorry'molsOrder12 : answer(sorry) ↔ HasCompleteMOLS 12 := by⊢ True ↔ HasCompleteMOLS 12
  sorryAll goals completed! 🐙


/-
TODO(rao107): Conjecture 8.5 in [Wa2011]:
Every latin square has the maximum number of disjoint duplexes. In particular, every latin square of
even order has a 2-partition and every latin square of odd order has a
(2, 2, 2, ..., 2, 1)-partition.
-/

/-
TODO(rao107): Conjecture 8.6 in [Wa2011]:
For all even $n > 4$ there exists a latin square of ordern $n$ which has no transversal but does
contain a 3-plex.
-/

/-
TODO(rao107): Conjecture 9.2 in [Wa2011]:
If $n$ is even, then $f(n, 2) = n$; if $n$ is odd, then $f(n, 2) > n$.
-/

/-
TODO(rao107): Conjecture 10.10 in [Wa2011]:
Every latin hypercube of odd dimension or of odd oder has a transversal.
-/

end LatinSquare