Hadamard Conjecture — Kronecker Product Closure

Sylvester's observation in full generality: if A and B are Hadamard matrices of orders m and n, then A ⊗ₖ B is a Hadamard matrix of order m * n, since

(A ⊗ₖ B)(A ⊗ₖ B)ᵀ = (A Aᵀ) ⊗ₖ (B Bᵀ) = (m I) ⊗ₖ (n I) = (m n) I.

So the set of Hadamard orders is closed under multiplication. This strictly extends the doubling family of Hadamard.Constructions: for example order 144 = 12 × 12 is reachable here, but is not of the form 2 ^ t (q + 1) for any prime power q ≡ 3 (mod 4) (the odd part of 144 is 9, and 8 is not such a prime power), so neither doubling nor Paley I alone produces it.

theorem Hadamard.hasHadamardMatrix_mul {m n : ℕ} (hm : HasHadamardMatrix m) (hn : HasHadamardMatrix n) : HasHadamardMatrix (m * n)

Closure under Kronecker products (Sylvester): the set of Hadamard orders is closed under multiplication.

theorem Hadamard.hasHadamardMatrix_oneFourFour : HasHadamardMatrix 144

A Hadamard matrix of order 144 = 12 × 12 exists. This order is not reachable from the doubling and Paley I families alone.