Hadamard Conjecture — Transport Across Index Types #
Constructions (Paley, Williamson, …) naturally produce square matrices
indexed by structured types such as Unit ⊕ F or products, while the
project's existence predicate HasHadamardMatrix n quantifies over
matrices indexed by Fin n. This file provides the transport lemma:
a Hadamard matrix over any finite index type of cardinality n yields
HasHadamardMatrix n, via Matrix.reindex along an equivalence.
theorem
Hadamard.hasHadamardMatrix_of_card
{ι : Type u_1}
[Fintype ι]
[DecidableEq ι]
{n : ℕ}
(hcard : Fintype.card ι = n)
(H : Matrix ι ι ℤ)
(hent : ∀ (i j : ι), H i j = 1 ∨ H i j = -1)
(horth : H * H.transpose = ↑n • 1)
:
A ±1 matrix over an arbitrary finite index type ι satisfying the
Hadamard orthogonality equation yields a Hadamard matrix of order
Fintype.card ι.