Hadamard Conjecture — Quadratic Character Sums and the Jacobsthal Matrix

This file develops the character-sum machinery behind the Paley construction of Hadamard matrices.

For a finite field F of odd cardinality q, let χ be the quadratic character of F (χ(0) = 0, χ(x) = 1 for nonzero squares, -1 otherwise). The Jacobsthal matrix is the q × q integer matrix Q x y = χ(x - y). The results proved here:

• quadraticChar_sum_shift_mul (Jacobsthal's lemma): for c ≠ 0, ∑ x, χ(x) χ(x + c) = -1. The proof substitutes x = (-c) · t, which identifies the sum with χ(-1) * J(χ, χ) for the Jacobi sum J, and then uses Mathlib's jacobiSum_nontrivial_inv : J(χ, χ⁻¹) = -χ(-1) together with the fact that the quadratic character is its own inverse.
• jacobsthal_row_sum, jacobsthal_col_sum: rows and columns of Q sum to zero (since ∑ χ = 0).
• jacobsthal_mul_transpose_apply: Q Qᵀ = q I - J entrywise, i.e. row x dotted with row y is q - 1 if x = y and -1 otherwise.
• jacobsthal_transpose: when q ≡ 3 (mod 4), Q is skew-symmetric (χ(-1) = -1).

These are the standard properties from Paley's 1933 paper On orthogonal matrices; the Jacobi-sum route follows Ireland–Rosen, A Classical Introduction to Modern Number Theory, Chapter 8.

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

Character sums

theorem Hadamard.ringChar_ne_two_of_card_mod_four_eq_three {F : Type u_1} [Field F] [Fintype F] (h3 : Fintype.card F % 4 = 3) : ringChar F ≠ 2

A finite field of cardinality ≡ 3 (mod 4) has odd characteristic.

theorem Hadamard.quadraticChar_neg_one_eq_neg_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (h3 : Fintype.card F % 4 = 3) : (quadraticChar F) (-1) = -1

If #F ≡ 3 (mod 4), the quadratic character of F is odd: χ(-1) = -1.

theorem Hadamard.quadraticChar_sum_shift_mul {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {c : F} (hc : c ≠ 0) : ∑ x : F, (quadraticChar F) x * (quadraticChar F) (x + c) = -1

Jacobsthal's lemma: over a finite field of odd characteristic, the shifted product of quadratic-character values sums to -1 for any nonzero shift c: ∑ x, χ(x) χ(x + c) = -1.

The substitution x = (-c) · t turns the left-hand side into χ(-1) * ∑ t, χ(t) χ(1 - t) = χ(-1) * jacobiSum χ χ, and jacobiSum χ χ = jacobiSum χ χ⁻¹ = -χ(-1) by Mathlib's Jacobi-sum evaluation, so the total is -χ(-1)² = -1.

The Jacobsthal matrix

def Hadamard.jacobsthal (F : Type u_1) [Field F] [Fintype F] [DecidableEq F] : Matrix F F ℤ

The Jacobsthal matrix of a finite field F: the square matrix indexed by F whose (x, y) entry is χ(x - y), where χ is the quadratic character of F. Its diagonal is 0 and all other entries are ±1.

Equations

• Hadamard.jacobsthal F = Matrix.of fun (x y : F) => (quadraticChar F) (x - y)

@[simp]

theorem Hadamard.jacobsthal_apply {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (x y : F) : jacobsthal F x y = (quadraticChar F) (x - y)

theorem Hadamard.jacobsthal_row_sum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (x : F) : ∑ y : F, jacobsthal F x y = 0

Rows of the Jacobsthal matrix sum to zero.

theorem Hadamard.jacobsthal_col_sum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (y : F) : ∑ x : F, jacobsthal F x y = 0

Columns of the Jacobsthal matrix sum to zero.

theorem Hadamard.jacobsthal_inner {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (x y : F) : ∑ z : F, jacobsthal F x z * jacobsthal F y z = if x = y then ↑(Fintype.card F) - 1 else -1

Inner products of rows of the Jacobsthal matrix: row x dotted with row y is q - 1 on the diagonal and -1 off it. Equivalently, Q Qᵀ = q I - J where J is the all-ones matrix.

theorem Hadamard.jacobsthal_transpose {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (h3 : Fintype.card F % 4 = 3) : (jacobsthal F).transpose = -jacobsthal F

When #F ≡ 3 (mod 4), the Jacobsthal matrix is skew-symmetric: Qᵀ = -Q.