Designs, Latin squares and combinatorial matrices

Block designs, Steiner systems, pairwise balanced designs and linear spaces, Latin squares and transversals, Hadamard and partial Hadamard matrices, magic squares, 0-1 matrices with prescribed margins (Gale–Ryser), binary matrices up to rotation, and sign tables from determinant-moment expansions; cyclic difference sets go to Sidon sets and difference sets.

TheoremCounting binary matrices up to cyclic rotations#✓fully proved

Let \(m, n \ge 1\). For an \(m \times n\) matrix \(x\) with entries \(x_{r,s} \in \{0, 1\}\), rows indexed by \(0 \le r < m\) and columns by \(0 \le s < n\), put \(N(x) = \sum_{r=0}^{m-1} \sum_{s=0}^{n-1} x_{r,s} \, 2^{rn+s}\), and for \(0 \le i < m\), \(0 \le j < n\) let \(x^{(i,j)}\) be the rotated matrix with entries \(x^{(i,j)}_{r,s} = x_{(r+i) \bmod m, \, (s+j) \bmod n}\). The number of such matrices \(x\) with \(N(x) \le N(x^{(i,j)})\) for all \(i\) and \(j\) equals

\[\left\lfloor \frac{1}{mn} \sum_{c \mid m} \sum_{d \mid n} \varphi(c) \, \varphi(d) \, 2^{mn / \operatorname{lcm}(c,d)} \right\rfloor,\]

where \(\varphi\) is Euler's totient function.

Since \(N\) is injective, each orbit under the cyclic row and column rotations contains exactly one such matrix, so this is the number of binary \(m \times n\) matrices up to rotation; by Burnside's lemma the division is exact (the Pólya enumeration formula).

theorem binaryMatrixRotationOrbitCount
    (m n : ℕ) (hm : 0 < m) (hn : 0 < n) :
    (Finset.univ.filter (fun x : Fin m → Fin n → Bool =>
      ∀ i : Fin m, ∀ j : Fin n,
        (∑ r : Fin m, ∑ s : Fin n,
          (if x r s = true then 1 else 0) * 2 ^ (r.val * n + s.val)) ≤
        (∑ r : Fin m, ∑ s : Fin n,
          (if x (r + i) (s + j) = true then 1 else 0) *
            2 ^ (r.val * n + s.val)))).card =
      (∑ c ∈ m.divisors, ∑ d ∈ n.divisors,
        Nat.totient c * Nat.totient d *
          2 ^ ((m * n) / Nat.lcm c d)) / (m * n)
Sources

TheoremMann's product criterion for orthogonal Latin squares#✓fully proved

Let \(n\) be a natural number, write \([n] = \{0, \dots, n-1\}\), and let \(A\) and \(B\) be Latin squares of order \(n\) with rows, columns and entries indexed by \([n]\): every row and every column of each square is a bijection of \([n]\). For a row index \(i\) write \(A_i\) and \(B_i\) for the permutations \(j \mapsto A_{ij}\) and \(j \mapsto B_{ij}\) of \([n]\). Then the map \((i, j) \mapsto (A_{ij}, B_{ij})\) is a bijection of \([n] \times [n]\) (that is, \(A\) and \(B\) are orthogonal) if and only if the square \(C\) with entries \(C_{ij} = A_i(B_i^{-1}(j))\) is a Latin square, meaning that every row \(j \mapsto C_{ij}\) and every column \(i \mapsto C_{ij}\) of \(C\) is a bijection of \([n]\).

The equivalence uses only the row conditions on \(A\) and \(B\); the column conditions are kept so that both inputs are Latin squares. The row condition on \(C\) follows from the row conditions on \(A\) and \(B\), and is included so that the right side is the full Latin-square condition.

theorem mann_product_criterion_for_orthogonal_latin_squares
    {n : ℕ} (A B : Fin n → Fin n → Fin n)
    (hArow : ∀ i, Function.Bijective (A i))
    (_hAcol : ∀ j, Function.Bijective (fun i => A i j))
    (hBrow : ∀ i, Function.Bijective (B i))
    (_hBcol : ∀ j, Function.Bijective (fun i => B i j)) :
    Function.Bijective (fun ij : Fin n × Fin n => (A ij.1 ij.2, B ij.1 ij.2)) ↔
      ((∀ i, Function.Bijective
          (fun j => A i ((Equiv.ofBijective (B i) (hBrow i)).symm j))) ∧
        ∀ j, Function.Bijective
          (fun i => A i ((Equiv.ofBijective (B i) (hBrow i)).symm j)))
2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.