Documentation

Hadamard.Paley

Hadamard Conjecture — The Paley Construction (Type I) #

Let F be a finite field with q = #F ≡ 3 (mod 4) and let Q be its Jacobsthal matrix (Hadamard.jacobsthal). Index (q+1) × (q+1) matrices by Unit ⊕ F and set

S = fromBlocks 0 1 (-1) Q, H = I + S.

Since q ≡ 3 (mod 4), the matrix S is skew-symmetric (Sᵀ = -S), and the character-sum identities give S Sᵀ = q I. Hence

H Hᵀ = (I + S)(I + Sᵀ) = I + S + Sᵀ + S Sᵀ = (q + 1) I,

and all entries of H are ±1 (the diagonal of S vanishes and is repaired by I). This is Paley's construction I (Paley, On orthogonal matrices, J. Math. Phys. 12 (1933), 311–320): a Hadamard matrix of order q + 1 for every prime power q ≡ 3 (mod 4), giving in particular orders 4, 8, 12, 20, 24, 28, 32, 44, 48, 60, 68, ….

Reference: https://en.wikipedia.org/wiki/Paley_construction

source
def Hadamard.paleySkew (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] :
Matrix (Unit ⊕ F) (Unit ⊕ F) ℤ

The skew companion of the Paley matrix: in block form (indexing by Unit ⊕ F), the top-left entry is 0, the first row is 1, the first column is -1, and the core is the Jacobsthal matrix.

Equations
Instances For
    source
    def Hadamard.paleyMatrix (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] :
    Matrix (Unit ⊕ F) (Unit ⊕ F) ℤ

    The Paley matrix of order #F + 1: identity plus the skew companion.

    Equations
    Instances For
      source
      theorem Hadamard.paleySkew_transpose {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (h3 : Fintype.card F % 4 = 3) :
      (paleySkew F).transpose = -paleySkew F

      For #F ≡ 3 (mod 4) the Paley skew companion is skew-symmetric.

      source
      theorem Hadamard.paleySkew_mul_transpose {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) :
      paleySkew F * (paleySkew F).transpose = ↑(Fintype.card F) • 1

      The key orthogonality computation: S Sᵀ = q I for the Paley skew companion. Top-left: the all-ones row dotted with itself gives q. Off-diagonal blocks: row/column sums of the Jacobsthal matrix vanish. Bottom-right: J + Q Qᵀ = J + (q I - J) = q I.

      source
      theorem Hadamard.paleyMatrix_mul_transpose {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (h3 : Fintype.card F % 4 = 3) :
      paleyMatrix F * (paleyMatrix F).transpose = ↑(Fintype.card F + 1) • 1

      The Paley matrix satisfies the Hadamard orthogonality equation H Hᵀ = (q + 1) I.

      source
      theorem Hadamard.paleyMatrix_entry {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (i j : Unit ⊕ F) :
      paleyMatrix F i j = 1 ∨ paleyMatrix F i j = -1

      All entries of the Paley matrix are ±1.

      source
      theorem Hadamard.hasHadamardMatrix_card_succ {F : Type u_1} [Field F] [Fintype F] (h3 : Fintype.card F % 4 = 3) :
      HasHadamardMatrix (Fintype.card F + 1)

      Paley construction I (Paley 1933): if F is a finite field with #F ≡ 3 (mod 4), then there is a Hadamard matrix of order #F + 1.

      source
      theorem Hadamard.hasHadamardMatrix_prime_pow_succ {p k : ℕ} (hp : Nat.Prime p) (hk : k ≠ 0) (h3 : p ^ k % 4 = 3) :
      HasHadamardMatrix (p ^ k + 1)

      Paley I for prime powers: for every prime power q = p ^ k with q ≡ 3 (mod 4) there is a Hadamard matrix of order q + 1. The witness field is the Galois field GaloisField p k.

      source
      theorem Hadamard.hasHadamardMatrix_twelve :
      HasHadamardMatrix 12

      A Hadamard matrix of order 12 exists (Paley, q = 11). This is the first order not reachable by the Sylvester doubling family.

      source
      theorem Hadamard.hasHadamardMatrix_twenty :
      HasHadamardMatrix 20

      A Hadamard matrix of order 20 exists (Paley, q = 19).

      source
      theorem Hadamard.hasHadamardMatrix_twentyEight :
      HasHadamardMatrix 28

      A Hadamard matrix of order 28 exists (Paley, q = 27 = 3³): a case that genuinely needs a non-prime prime power.