Hadamard Conjecture — Equivalent Forms

Two convenient formulations:

• every order divisible by 4 admits a Hadamard matrix,
• every order of the form 4k admits a Hadamard matrix.
• the classical admissible-order form (1, 2, or multiple of 4).

All quantification is over natural numbers.

def Hadamard.HadamardConjectureMul4 : Prop

Multiplicative form: every order 4k is realizable.

Equations

• Hadamard.HadamardConjectureMul4 = ∀ (k : ℕ), Hadamard.HasHadamardMatrix (4 * k)

def Hadamard.HadamardConjectureDvd : Prop

Divisibility form: every order divisible by 4 is realizable.

Equations

• Hadamard.HadamardConjectureDvd = ∀ (n : ℕ), 4 ∣ n → Hadamard.HasHadamardMatrix n

theorem Hadamard.hadamardConjectureMul4_implies_dvd : HadamardConjectureMul4 → HadamardConjectureDvd

theorem Hadamard.hadamardConjectureDvd_implies_mul4 : HadamardConjectureDvd → HadamardConjectureMul4

theorem Hadamard.hadamardConjectureMul4_iff_dvd : HadamardConjectureMul4 ↔ HadamardConjectureDvd

def Hadamard.HadamardConjectureClassical : Prop

Classical form: every admissible order (1, 2, or multiple of 4) is realizable.

Equations

• Hadamard.HadamardConjectureClassical = ∀ (n : ℕ), Hadamard.HadamardOrderAdmissible n → Hadamard.HasHadamardMatrix n

theorem Hadamard.hadamardConjectureClassical_implies_dvd : HadamardConjectureClassical → HadamardConjectureDvd

theorem Hadamard.hadamardConjectureDvd_implies_classical : HadamardConjectureDvd → HadamardConjectureClassical

theorem Hadamard.hadamardConjectureDvd_iff_classical : HadamardConjectureDvd ↔ HadamardConjectureClassical

def Hadamard.HadamardNecessaryCondition : Prop

Standard necessary-condition statement from the literature.

Equations

• Hadamard.HadamardNecessaryCondition = ∀ (n : ℕ), Hadamard.HasHadamardMatrix n → Hadamard.HadamardOrderAdmissible n

def Hadamard.HadamardDeterminantCharacterization : Prop

Standard determinant characterization statement from the literature.

Equations

• Hadamard.HadamardDeterminantCharacterization = ∀ (n : ℕ) (H : Matrix (Fin n) (Fin n) ℤ), Hadamard.IsHadamardMatrix n H ↔ Hadamard.IsHadamardMatrixDeterminantForm n H

def Hadamard.HadamardNormalizationEquivalence : Prop

Standard normalization equivalence statement for nonempty orders.

Equations

• Hadamard.HadamardNormalizationEquivalence = ∀ (n : ℕ), 0 < n → (Hadamard.HasHadamardMatrix n ↔ Hadamard.HasNormalizedHadamardMatrix n)

@[reducible, inline]

abbrev Hadamard.HadamardConjecture : Prop

The project's primary statement of the Hadamard conjecture.

Equations

• Hadamard.HadamardConjecture = Hadamard.HadamardConjectureDvd