Hadamard matrices

DefinitionHadamard matrix#✓fully proved

For a natural number \(m\), an \(m \times m\) matrix \(H\) with integer entries is a Hadamard matrix when every entry of \(H\) is \(1\) or \(-1\) and \(H^{\mathsf T} H = m I\), where \(I\) is the \(m \times m\) identity matrix.

This predicate is used for Hadamard matrices of order \(n + 1\) with circulant core, which exist when \(n\) is a prime congruent to \(3\) mod \(4\) (Paley) or \(n = p(p + 2)\) with \(p\) and \(p + 2\) both prime (Stanton–Sprott/Whiteman).

public def isHadamardMatrix (m : ℕ) (H : Matrix (Fin m) (Fin m) ℤ) : Prop :=
  (∀ i j, H i j = 1 ∨ H i j = -1) ∧
    (Matrix.transpose H) * H = (m : ℤ) • (1 : Matrix (Fin m) (Fin m) ℤ)

Sources

• Richard P. Brent and Adam B. Yedidia, "Computation of Maximal Determinants of Binary Circulant Matrices," Journal of Integer Sequences 21 (2018), Article 18.5.6, Theorem, lines 684–695, https://cs.uwaterloo.ca/journals/JIS/VOL21/Brent/brent11.tex quoting Kotsireas et al.; attributions at lines 698–704. The prime-power versions of cases (1)–(2), if the source allows them, and cases (3)–(4) of the source theorem (Singer, Hall) are not part of this statement.

Used by 3

Used byHadamard matrices with circulant core: Paley and twin-prime cases · Circulant-core Hadamard matrices with orthogonal rows and columns · One-sided orthogonality characterizes Hadamard matrices

TheoremHadamard matrices with circulant core: Paley and twin-prime cases#✓fully proved

Let \(n\) be a natural number such that either \(n\) is a prime with \(n \equiv 3 \pmod 4\), or \(n = p(p + 2)\) for some natural number \(p\) with \(p\) and \(p + 2\) both prime. Then there is an \((n + 1) \times (n + 1)\) Hadamard matrix \(H\) with integer entries, rows and columns indexed by \(0, 1, \dots, n\) (so every entry of \(H\) is \(1\) or \(-1\) and \(H^{\mathsf T} H = (n + 1) I\)), that has a circulant core: there is a function \(v \colon \{0, \dots, n - 1\} \to \mathbb{Z}\) with \(H_{i+1, j+1} = v(i - j)\) for all \(i, j \in \{0, \dots, n - 1\}\), where \(i - j\) is taken modulo \(n\).

public theorem exists_hadamard_matrix_with_circulant_core :
    ∀ (n : ℕ),
      ((Nat.Prime n ∧ n % 4 = 3) ∨
          (∃ p : ℕ, Nat.Prime p ∧ Nat.Prime (p + 2) ∧ n = p * (p + 2))) →
        ∃ H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ,
          isHadamardMatrix (n + 1) H ∧ hasCirculantCore n H

Uses 1 · Used by 1

Statement usesHadamard matrix

Used byCirculant-core Hadamard matrices with orthogonal rows and columns

TheoremOne-sided orthogonality characterizes Hadamard matrices#✓fully proved

Let \(m\) be a natural number and let \(H\) be an \(m \times m\) integer matrix. Then every entry of \(H\) is \(1\) or \(-1\) and \(H^{\mathsf T} H = m I\) if and only if every entry of \(H\) is a unitary element of \(\mathbb{Z}\) (that is, \(1\) or \(-1\)), \(H H^{\mathsf T} = m I\) and \(H^{\mathsf T} H = m I\). The right-hand side is the general notion of a Hadamard matrix, with entries unitary and \(H H^{*} = H^{*} H = m I\); over \(\mathbb{Z}\) the conjugate transpose \(H^{*}\) is the transpose.

public theorem isHadamardMatrix_iff_isHadamard {m : ℕ} {H : Matrix (Fin m) (Fin m) ℤ} :
    isHadamardMatrix m H ↔ H.IsHadamard

Uses 1 · Used by 1

Statement usesHadamard matrix

Used byCirculant-core Hadamard matrices with orthogonal rows and columns

TheoremA circulant core is a circulant submatrix#✓fully proved

Let \(n\) be a natural number and let \(H\) be an \((n + 1) \times (n + 1)\) integer matrix with rows and columns indexed by \(0, 1, \dots, n\). Then \(H\) has a circulant core, meaning that there is a function \(v \colon \{0, \dots, n - 1\} \to \mathbb{Z}\) with \(H_{i+1, j+1} = v(i - j)\) for all \(i, j \in \{0, \dots, n - 1\}\), if and only if there is a function \(v \colon \{0, \dots, n - 1\} \to \mathbb{Z}\) such that the submatrix \((H_{i+1, j+1})_{0 \le i, j \le n - 1}\) equals the circulant matrix of \(v\), whose \((i, j)\) entry is \(v(i - j)\). In both conditions \(i - j\) is taken modulo \(n\).

public theorem hasCirculantCore_iff_circulant {n : ℕ}
    {H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ} :
    hasCirculantCore n H ↔
      ∃ v : Fin n → ℤ, H.submatrix Fin.succ Fin.succ = Matrix.circulant v

Used by 1

Used byCirculant-core Hadamard matrices with orthogonal rows and columns

TheoremCirculant-core Hadamard matrices with orthogonal rows and columns#✓fully proved

Let \(n\) be a natural number such that either \(n\) is a prime with \(n \equiv 3 \pmod 4\), or \(n = p(p + 2)\) for some natural number \(p\) with \(p\) and \(p + 2\) both prime. Then there is an \((n + 1) \times (n + 1)\) integer matrix \(H\), with rows and columns indexed by \(0, 1, \dots, n\), such that every entry of \(H\) is \(1\) or \(-1\), \(H H^{\mathsf T} = (n + 1) I\) and \(H^{\mathsf T} H = (n + 1) I\), and there is a function \(v \colon \{0, \dots, n - 1\} \to \mathbb{Z}\) such that the submatrix \((H_{i+1, j+1})_{0 \le i, j \le n - 1}\) obtained by deleting row \(0\) and column \(0\) equals the circulant matrix of \(v\), whose \((i, j)\) entry is \(v(i - j)\) with \(i - j\) taken modulo \(n\).

public theorem exists_isHadamard_with_circulant_core :
    ∀ (n : ℕ),
      ((Nat.Prime n ∧ n % 4 = 3) ∨
          (∃ p : ℕ, Nat.Prime p ∧ Nat.Prime (p + 2) ∧ n = p * (p + 2))) →
        ∃ H : Matrix (Fin (n + 1)) (Fin (n + 1)) ℤ,
          H.IsHadamard ∧ ∃ v : Fin n → ℤ,
            H.submatrix Fin.succ Fin.succ = Matrix.circulant v

Uses 4

Proof usesHadamard matrices with circulant core: Paley and twin-prime cases · A circulant core is a circulant submatrix · Hadamard matrix · One-sided orthogonality characterizes Hadamard matrices

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.