Hadamard Conjecture — First Constructions

This file contains baseline constructions and proved theorems for the Sylvester/Kronecker doubling pipeline.

def Hadamard.hadamardOne : Matrix (Fin 1) (Fin 1) ℤ

The unique 1 × 1 Hadamard matrix.

Equations

• Hadamard.hadamardOne x✝¹ x✝ = 1

theorem Hadamard.isHadamardMatrix_one : IsHadamardMatrix 1 hadamardOne

theorem Hadamard.hasHadamardMatrix_one : HasHadamardMatrix 1

def Hadamard.sylvesterTwo : Matrix (Fin 2) (Fin 2) ℤ

The 2 × 2 Sylvester seed matrix.

Equations

• Hadamard.sylvesterTwo = !![1, 1; 1, -1]

theorem Hadamard.sylvesterTwo_entry (i j : Fin 2) : sylvesterTwo i j = 1 ∨ sylvesterTwo i j = -1

theorem Hadamard.isHadamardMatrix_two : IsHadamardMatrix 2 sylvesterTwo

theorem Hadamard.hasHadamardMatrix_two : HasHadamardMatrix 2

theorem Hadamard.mul_eq_one_or_neg_one_of_eq_one_or_neg_one {a b : ℤ} (ha : a = 1 ∨ a = -1) (hb : b = 1 ∨ b = -1) : a * b = 1 ∨ a * b = -1

theorem Hadamard.hasHadamardMatrix_double_of_hasHadamardMatrix {n : ℕ} (h : HasHadamardMatrix n) : HasHadamardMatrix (2 * n)

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