Hadamard Conjecture — The Necessity Theorem

This file proves the classical necessary condition on the order of a Hadamard matrix: if an n × n Hadamard matrix exists, then n = 1, n = 2, or 4 ∣ n.

The proof is the standard three-row argument in a streamlined algebraic form. Given three distinct rows p, q, r of a Hadamard matrix H, consider

S = ∑ j, (H p j + H q j) * (H p j + H r j).

Expanding the product and using orthogonality of distinct rows together with ∑ j, H p j ^ 2 = n gives S = n. On the other hand each summand is a product of two even integers (each factor is a sum of two ±1s), hence divisible by 4. Therefore 4 ∣ n whenever n ≥ 3.

This is the counting lemma that goes back to Hadamard's 1893 paper; see also Stinson, Combinatorial Designs (2004), or Hall, Combinatorial Theory, Chapter 14.

Reference: https://en.wikipedia.org/wiki/Hadamard_matrix

theorem Hadamard.IsHadamardMatrix.row_inner {n : ℕ} {H : Matrix (Fin n) (Fin n) ℤ} (hH : IsHadamardMatrix n H) (p q : Fin n) : ∑ j : Fin n, H p j * H q j = if p = q then ↑n else 0

The defining orthogonality relation of a Hadamard matrix read off entrywise: the inner product of rows p and q is n if p = q and 0 otherwise.

theorem Hadamard.IsHadamardMatrix.four_dvd_term {n : ℕ} {H : Matrix (Fin n) (Fin n) ℤ} (hH : IsHadamardMatrix n H) (p q r j : Fin n) : 4 ∣ (H p j + H q j) * (H p j + H r j)

Each summand in the three-row sum is divisible by 4: both factors are sums of two ±1s, hence even.

theorem Hadamard.IsHadamardMatrix.four_dvd_order {n : ℕ} {H : Matrix (Fin n) (Fin n) ℤ} (hH : IsHadamardMatrix n H) (hn : 3 ≤ n) : 4 ∣ n

Three-row argument: a Hadamard matrix of order n ≥ 3 forces 4 ∣ n.

theorem Hadamard.hadamardNecessaryCondition_holds : HadamardNecessaryCondition

Necessity theorem for the Hadamard conjecture: the order of a Hadamard matrix is 1, 2, or a multiple of 4. This resolves the statement object HadamardNecessaryCondition.