Hadamard Conjecture — Main Results and Conjecture Stub

theorem Hadamard.hadamard_family_pow_two (k : ℕ) : HasHadamardMatrix (2 ^ k)

Confirmed infinite family: powers of two admit Hadamard matrices.

theorem Hadamard.hadamard_necessary : HadamardNecessaryCondition

Necessity (Hadamard 1893): the order of any Hadamard matrix is 1, 2, or a multiple of 4. Together with the conjecture stub below this explains why the conjecture quantifies over multiples of 4.

theorem Hadamard.hadamard_family_paley {p k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) (h3 : p ^ k % 4 = 3) : HasHadamardMatrix (p ^ k + 1)

Paley's infinite family (Paley 1933): for every prime power q = p ^ k ≡ 3 (mod 4) there is a Hadamard matrix of order q + 1. Combined with hadamard_family_pow_two and Sylvester doubling this covers all admissible orders up to 36, the first order needing Paley's second construction.

theorem Hadamard.hasHadamardMatrix_of_admissible_le_32 {n : ℕ} (hn : n ≤ 32) (h : HadamardOrderAdmissible n) : HasHadamardMatrix n

Checkpoint: every admissible order up to 32 admits a Hadamard matrix, by combining Sylvester powers of two, doubling, and Paley I. The first admissible order beyond the reach of the currently formalized families is 36, which requires Paley's second construction.

theorem Hadamard.hadamard_conjecture_iff_classical : HadamardConjecture ↔ HadamardConjectureClassical

The project's primary conjecture is equivalent to the classical 1/2/4k form.

theorem Hadamard.hadamard_conjecture : HadamardConjecture

Hadamard conjecture: every n divisible by 4 admits an n × n Hadamard matrix (formalized over n : ℕ).