Quasi-complete Latin squares from terraces (Bailey)

For a finite group G and orderings a, b : Fin |G| ≃ G, the Cayley table L(a, b) i j = a i * b j is quasi-complete (every unordered pair of distinct symbols is adjacent exactly twice horizontally and exactly twice vertically) if and only if a⁻¹ and b are terraces: for every g ≠ 1, g and g⁻¹ together occur exactly twice among the successive quotients (Theorem of the Day; R. A. Bailey 1984). Proof: horizontal neighbours (a_i b_j, a_i b_{j+1}) have quotient b_j⁻¹ b_{j+1}, vertical ones a_i a_{i+1}⁻¹, and for each fixed column or row the map to the first symbol is a bijection.

Main results

• Bailey.quasiComplete_iff: Bailey's theorem: L(a, b) quasi-complete iff a⁻¹ and b are terraces

References

• R. Whitty, Theorem of the Day, «Bailey's Theorem on Latin Squares» (Bailey).
• R. A. Bailey, «Quasi-complete Latin squares: construction and randomization», J. Roy. Statist. Soc. B 46 (1984) 323–334.

noncomputable def Bailey.diffCount {G : Type u_1} [Group G] [Fintype G] (s : Fin (Fintype.card G) ≃ G) (g : G) : ℕ

Número de posiciones k (con k + 1 < |G|) cuya diferencia sucesiva s k⁻¹ * s (k+1) es g.

Equations

• Bailey.diffCount s g = {k : Fin (Fintype.card G) | ∃ (h : ↑k + 1 < Fintype.card G), (s k)⁻¹ * s ⟨↑k + 1, h⟩ = g}.card

def Bailey.IsTerrace {G : Type u_1} [Group G] [Fintype G] (s : Fin (Fintype.card G) ≃ G) : Prop

Terraza: para todo g ≠ 1, g y g⁻¹ aparecen, juntos, exactamente dos veces entre las diferencias sucesivas (una involución aparece, pues, una sola vez).

Equations

• Bailey.IsTerrace s = ∀ (g : G), g ≠ 1 → Bailey.diffCount s g + Bailey.diffCount s g⁻¹ = 2

def Bailey.IsQuasiComplete {G : Type u_1} [Fintype G] (L : Fin (Fintype.card G) → Fin (Fintype.card G) → G) : Prop

Cuadrado casi completo: cada par no ordenado {x, y} de símbolos distintos aparece exactamente dos veces como vecinos horizontales y exactamente dos veces como vecinos verticales.

Equations

• One or more equations did not get rendered due to their size.

theorem Bailey.pair_iff {G : Type u_1} {u v x y : G} (hxy : x ≠ y) : {u, v} = {x, y} ↔ u = x ∧ v = y ∨ u = y ∧ v = x

theorem Bailey.card_horiz {G : Type u_1} [Group G] [Fintype G] (a b : Fin (Fintype.card G) ≃ G) (x y g : G) (hg : x⁻¹ * y = g) : {p : Fin (Fintype.card G) × Fin (Fintype.card G) | ∃ (h : ↑p.2 + 1 < Fintype.card G), a p.1 * b p.2 = x ∧ a p.1 * b ⟨↑p.2 + 1, h⟩ = y}.card = diffCount b g

Horizontal ordered count.

theorem Bailey.card_vert {G : Type u_1} [Group G] [Fintype G] (a b : Fin (Fintype.card G) ≃ G) (x y g : G) (hg : x * y⁻¹ = g) : {p : Fin (Fintype.card G) × Fin (Fintype.card G) | ∃ (h : ↑p.1 + 1 < Fintype.card G), a p.1 * b p.2 = x ∧ a ⟨↑p.1 + 1, h⟩ * b p.2 = y}.card = diffCount (a.trans (Equiv.inv G)) g

Vertical ordered count, for the list a⁻¹.

theorem Bailey.horiz_count {G : Type u_1} [Group G] [Fintype G] (a b : Fin (Fintype.card G) ≃ G) {x y : G} (hxy : x ≠ y) : {p : Fin (Fintype.card G) × Fin (Fintype.card G) | ∃ (h : ↑p.2 + 1 < Fintype.card G), {a p.1 * b p.2, a p.1 * b ⟨↑p.2 + 1, h⟩} = {x, y}}.card = diffCount b (x⁻¹ * y) + diffCount b (y⁻¹ * x)

theorem Bailey.vert_count {G : Type u_1} [Group G] [Fintype G] (a b : Fin (Fintype.card G) ≃ G) {x y : G} (hxy : x ≠ y) : {p : Fin (Fintype.card G) × Fin (Fintype.card G) | ∃ (h : ↑p.1 + 1 < Fintype.card G), {a p.1 * b p.2, a ⟨↑p.1 + 1, h⟩ * b p.2} = {x, y}}.card = diffCount (a.trans (Equiv.inv G)) (x * y⁻¹) + diffCount (a.trans (Equiv.inv G)) (y * x⁻¹)

theorem Bailey.quasiComplete_iff {G : Type u_1} [Group G] [Fintype G] (a b : Fin (Fintype.card G) ≃ G) : (IsQuasiComplete fun (i j : Fin (Fintype.card G)) => a i * b j) ↔ IsTerrace (a.trans (Equiv.inv G)) ∧ IsTerrace b