Hadamard Conjecture — Core Definitions

This file defines Hadamard matrices over ℤ using the classical ±1 entry condition and orthogonality equation.

def Hadamard.IsHadamardMatrix (n : ℕ) (H : Matrix (Fin n) (Fin n) ℤ) : Prop

A square n × n integer matrix is Hadamard if every entry is ±1 and H * Hᵀ = n I.

Equations

• Hadamard.IsHadamardMatrix n H = ((∀ (i j : Fin n), H i j = 1 ∨ H i j = -1) ∧ H * H.transpose = ↑n • 1)

def Hadamard.HasHadamardMatrix (n : ℕ) : Prop

Existence predicate for Hadamard matrices of order n.

Equations

• Hadamard.HasHadamardMatrix n = ∃ (H : Matrix (Fin n) (Fin n) ℤ), Hadamard.IsHadamardMatrix n H

def Hadamard.HadamardOrderAdmissible (n : ℕ) : Prop

Classical admissible orders for real Hadamard matrices: 1, 2, or a multiple of 4.

Equations

• Hadamard.HadamardOrderAdmissible n = (n = 1 ∨ n = 2 ∨ 4 ∣ n)

def Hadamard.IsNormalizedHadamardMatrix (n : ℕ) (H : Matrix (Fin n) (Fin n) ℤ) : Prop

Normalized Hadamard matrices have all first-row/first-column entries equal to 1.

Equations

• Hadamard.IsNormalizedHadamardMatrix n H = (Hadamard.IsHadamardMatrix n H ∧ ∀ (i j : Fin n), ↑i = 0 ∨ ↑j = 0 → H i j = 1)

def Hadamard.HasNormalizedHadamardMatrix (n : ℕ) : Prop

Existence predicate for normalized Hadamard matrices of order n.

Equations

• Hadamard.HasNormalizedHadamardMatrix n = ∃ (H : Matrix (Fin n) (Fin n) ℤ), Hadamard.IsNormalizedHadamardMatrix n H

def Hadamard.IsHadamardMatrixDeterminantForm (n : ℕ) (H : Matrix (Fin n) (Fin n) ℤ) : Prop

Determinant-form characterization used in the literature.

Equations

• Hadamard.IsHadamardMatrixDeterminantForm n H = ((∀ (i j : Fin n), H i j = 1 ∨ H i j = -1) ∧ H.det.natAbs = n ^ (n / 2))

theorem Hadamard.IsNormalizedHadamardMatrix.isHadamard {n : ℕ} {H : Matrix (Fin n) (Fin n) ℤ} (hH : IsNormalizedHadamardMatrix n H) : IsHadamardMatrix n H

theorem Hadamard.hasHadamardMatrix_of_hasNormalizedHadamardMatrix {n : ℕ} (h : HasNormalizedHadamardMatrix n) : HasHadamardMatrix n