Hadamard matrices of order $4t$ from four symmetric $\pm1$ sequences

Proved

Williamson_of_sequences

by ronr · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsdesign-theoryhadamard-matrixlinear-algebra

This reduces the construction of a Hadamard matrix of order $4t$ to a purely sequence-level condition, removing all matrix reasoning from the search for Williamson quadruples.

Let $a,b,c,d:\mathbb{Z}/t\mathbb{Z}\to\mathbb{R}$ be four sequences such that:

every value of each sequence is $1$ or $-1$ ;
each is symmetric, $a(-i)=a(i)$ and likewise for $b,c,d$ ; and
their periodic autocorrelations sum to zero off the origin:

\sum_{j\in\mathbb{Z}/t\mathbb{Z}}\bigl(a(i-j)a(j)+b(i-j)b(j)+c(i-j)c(j)+d(i-j)d(j)\bigr)=\begin{cases}4t,&i=0,\\0,&i\neq0.\end{cases}

Then there is a Hadamard matrix of order $4t$ : a $4t\times4t$ matrix with all entries $\pm1$ satisfying $MM^{\mathsf T}=4t\,I_{4t}$ .

Why this is the useful form. Taking $A,B,C,D$ to be the circulant matrices generated by $a,b,c,d$ , condition (2) makes them symmetric, circulants always commute, and condition (3) is exactly the matrix identity $A^{2}+B^{2}+C^{2}+D^{2}=4t\,I_{t}$ rewritten at the level of generating vectors. Williamson's array (Williamson_array) then assembles them into the order- $4t$ Hadamard matrix.

The practical consequence is that verifying a candidate Williamson quadruple no longer requires any $t\times t$ matrix algebra: it requires only checking $t-1$ scalar identities among four $\pm1$ sequences. This is the standard interface through which known Williamson quadruples — which exist for many $t$ not covered by the Sylvester or Paley constructions, classically $t=23$ giving order $92$ — are turned into Hadamard matrices.

Formalization Note The sequences are indexed by ZMod t so that the shift $i-j$ is the periodic one; NeZero t supplies the Fintype instance. The proof uses Mathlib's Matrix.circulant API: circulant_mul_comm gives commutativity for free, circulant_isSymm_iff converts condition (2), and circulant_mul together with circulant_inj converts condition (3) from a matrix identity to the displayed vector identity. The result is transported from the natural index type $(\mathbb{Z}/t\mathbb{Z}\oplus\mathbb{Z}/t\mathbb{Z})\oplus(\mathbb{Z}/t\mathbb{Z}\oplus\mathbb{Z}/t\mathbb{Z})$ to Fin (4*t).

Preamble

import Mathlib
open Matrix

Formal statement

theorem Williamson_of_sequences (t : ℕ) [NeZero t] (a b c d : ZMod t → ℝ)
    (hapm : ∀ i, a i = 1 ∨ a i = -1) (hbpm : ∀ i, b i = 1 ∨ b i = -1)
    (hcpm : ∀ i, c i = 1 ∨ c i = -1) (hdpm : ∀ i, d i = 1 ∨ d i = -1)
    (hasy : ∀ i, a (-i) = a i) (hbsy : ∀ i, b (-i) = b i)
    (hcsy : ∀ i, c (-i) = c i) (hdsy : ∀ i, d (-i) = d i)
    (hauto : ∀ i : ZMod t, (∑ j : ZMod t,
        (a (i - j) * a j + b (i - j) * b j + c (i - j) * c j + d (i - j) * d j)) =
      if i = 0 then (4 * t : ℝ) else 0) :
    ∃ M : Matrix (Fin (4 * t)) (Fin (4 * t)) ℝ,
      (∀ i j, M i j = 1 ∨ M i j = -1) ∧
        M * Mᵀ = ((4 * t : ℕ) : ℝ) • (1 : Matrix (Fin (4 * t)) (Fin (4 * t)) ℝ) := by sorry

Source

J. Williamson, Hadamard's determinant theorem and the sum of four squares, Duke Math. J. 11 (1944), 65-81. The reformulation of the sum-of-squares condition as a periodic autocorrelation condition on the four generating sequences is standard; see K. J. Horadam, Hadamard Matrices and Their Applications, Princeton University Press, 2007, Section 4.1, or J. Seberry and M. Yamada, Hadamard matrices, sequences, and block designs, in Contemporary Design Theory, Wiley, 1992. Built on the Prove2Me theorem Williamson_array (150f7786-c4d5-4a97-bb3e-15d34236a271).

View graph

Hadamard matrices of order 4t4t4t from four symmetric ±1\pm1±1 sequences

Hadamard matrices of order $4t$ from four symmetric $\pm1$ sequences