Williamson arrays imply Hadamard for odd orders

Open

exists_williamson_arrays_odd

by jackjburleson · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

For every odd integer $k \geq 3$ , suppose there exist four $k \times k$ symmetric circulant matrices $A, B, C, D$ with entries in $\{+1, -1\}$ such that they pairwise commute and satisfy

A^2 + B^2 + C^2 + D^2 = 4k \cdot I_k.

Then a Hadamard matrix of order $4k$ exists.This lemma connects Williamson array existence to Hadamard matrix construction, forming a key intermediate step in reducing the general Hadamard conjecture to the study of Williamson matrices at odd composite orders.

Preamble

import Mathlib.LinearAlgebra.Matrix.Kronecker
import Mathlib.Analysis.SpecialFunctions.Pow.Real

open Matrix

Formal statement

theorem exists_williamson_arrays_odd (k : ℕ) (hk_odd : Odd k) (hk_ge3 : 3 ≤ k) :
    ∃ A B C D : Matrix (Fin k) (Fin k) ℝ,
      (∀ i j, A i j = 1 ∨ A i j = -1) ∧
      (∀ i j, B i j = 1 ∨ B i j = -1) ∧
      (∀ i j, C i j = 1 ∨ C i j = -1) ∧
      (∀ i j, D i j = 1 ∨ D i j = -1) ∧
      A.transpose = A ∧ B.transpose = B ∧ C.transpose = C ∧ D.transpose = D ∧
      A * B = B * A ∧ A * C = C * A ∧ A * D = D * A ∧
      B * C = C * B ∧ B * D = D * B ∧ C * D = D * C ∧
      A * A + B * B + C * C + D * D = ((4 * k : ℕ) : ℝ) • (1 : Matrix (Fin k) (Fin k) ℝ) := by sorry

View graph