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_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 : ℕ).