Partial Hadamard matrices

DefinitionSign of a bit#✓fully proved

The sign of a bit \(b \in \{0, 1\}\) is the integer \(\sigma(b)\) given by \(\sigma(0) = -1\) and \(\sigma(1) = 1\).

def signVal (b : Fin 2) : ℤ := if b = 0 then -1 else 1

Used by 2

Used byPartial Hadamard matrices · Width-zero partial Hadamard count

DefinitionPartial Hadamard matrices#✓fully proved

Read a bit \(b \in \{0, 1\}\) as the sign \(\sigma(b)\), where \(\sigma(0) = -1\) and \(\sigma(1) = 1\). An \(n \times t\) matrix \(M\) with entries in \(\{0, 1\}\) is a partial Hadamard matrix when its rows are pairwise orthogonal as sign vectors: for all distinct rows \(i \ne i'\), \(\sum_{j < t} \sigma(M_{ij}) \sigma(M_{i'j}) = 0\).

def IsPartialHadamard {n t : ℕ} (M : Fin n → Fin t → Fin 2) : Prop :=
  ∀ i i' : Fin n, i ≠ i' →
    ∑ j : Fin t, signVal (M i j) * signVal (M i' j) = 0

Uses 1 · Used by 2

Statement usesSign of a bit

Used byNumber of partial Hadamard matrices · Width-zero partial Hadamard count

DefinitionNumber of partial Hadamard matrices#✓fully proved

For natural numbers \(n\) and \(t\), \(N_{n,t}\) is the number of \(n \times t\) partial Hadamard matrices, that is, of \(n \times t\) matrices with entries in \(\{0, 1\}\) whose rows are pairwise orthogonal when each entry \(0\) is read as the sign \(-1\) and each entry \(1\) as the sign \(1\).

noncomputable def partialHadamardCount (n t : ℕ) : ℕ :=
  Fintype.card { M : Fin n → Fin t → Fin 2 // IsPartialHadamard M }

Uses 1 · Used by 2

Statement usesPartial Hadamard matrices

Used byAdmissible exponents for the partial Hadamard leading term · Width-zero partial Hadamard count

TheoremWidth-zero partial Hadamard count#✓fully proved

For every natural number \(n\), the number \(N_{n,0}\) of \(n \times 0\) partial Hadamard matrices is \(1\): the orthogonality conditions are empty sums, so the empty matrix is the only one.

theorem partialHadamardCount_zero_width (n : ℕ) :
    partialHadamardCount n 0 = 1

Uses 3

Statement usesNumber of partial Hadamard matrices

Proof usesPartial Hadamard matrices · Sign of a bit

DefinitionDe Launey–Levin leading term#✓fully proved

For natural numbers \(n\) and \(t\), the de Launey–Levin leading term is the real number \(A_{n,4t} = 2^{4nt + (n-1)^2} (8\pi t)^{-n(n-1)/4}\), where the power of \(8\pi t\) is the real power function and \(n - 1\) in the exponent of \(2\) is truncated subtraction of natural numbers, so that \((n-1)^2 = 0\) when \(n = 0\).

noncomputable def leadingTerm (n t : ℕ) : ℝ :=
  (2 : ℝ) ^ (4 * n * t + (n - 1) ^ 2) *
    (8 * Real.pi * t) ^ (-((n * (n - 1) : ℝ) / 4))

Used by 1

Used byAdmissible exponents for the partial Hadamard leading term

DefinitionAdmissible exponents for the partial Hadamard leading term#✓fully proved

For natural numbers \(n\) and \(m\), let \(N_{n,m}\) be the number of \(n \times m\) partial Hadamard matrices, and for natural numbers \(n\) and \(t\) let \(A_{n,4t} = 2^{4nt + (n-1)^2} (8\pi t)^{-n(n-1)/4}\) be the de Launey–Levin leading term. A real number \(\alpha\) is admissible for the leading term when, for all sequences \((n_k)\) and \((t_k)\) of natural numbers with \(n_k \ge 2\) for every \(k\) and \(t_k / n_k^{\alpha} \to \infty\) as \(k \to \infty\), the ratio \(N_{n_k, 4t_k} / A_{n_k, 4t_k}\) tends to \(1\).

The catalogue constant \(C_{23c}\) also allows corrected asymptotic formulas below the cubic scale; this predicate is its precise leading-term specialization, whose exact threshold the source records as \(3\).

def IsLeadingAdmissible (α : ℝ) : Prop :=
  ∀ (n t : ℕ → ℕ), (∀ k : ℕ, 2 ≤ n k) →
    Tendsto (fun k : ℕ => (t k : ℝ) / (n k : ℝ) ^ α) atTop atTop →
    Tendsto (fun k : ℕ =>
      (partialHadamardCount (n k) (4 * t k) : ℝ) / leadingTerm (n k) (t k))
      atTop (nhds 1)

Uses 2 · Used by 3

Statement usesDe Launey–Levin leading term · Number of partial Hadamard matrices

Used byPartial Hadamard counts follow the leading term above the cubic scale · No exponent below 3 is admissible for the partial Hadamard leading term · Leading-term counting exponent for partial Hadamard matrices

DefinitionLeading-term counting exponent for partial Hadamard matrices#✓fully proved

For natural numbers \(n\) and \(m\), let \(N_{n,m}\) be the number of \(n \times m\) partial Hadamard matrices, and for natural numbers \(n\) and \(t\) let \(A_{n,4t} = 2^{4nt + (n-1)^2} (8\pi t)^{-n(n-1)/4}\) be the de Launey–Levin leading term. Call a real number \(\alpha\) admissible when \(N_{n_k, 4t_k} / A_{n_k, 4t_k} \to 1\) along all sequences \((n_k)\) and \((t_k)\) of natural numbers with \(n_k \ge 2\) for every \(k\) and \(t_k / n_k^{\alpha} \to \infty\). The leading-term counting exponent is the infimum of the admissible \(\alpha \ge 1\), and is \(0\) if there is no such \(\alpha\).

This exponent is not asserted to equal the catalogue constant \(C_{23c}\), which also permits corrected asymptotic formulas.

noncomputable def leadingTermExponent : ℝ :=
  sInf { α : ℝ | 1 ≤ α ∧ IsLeadingAdmissible α }

Uses 1

Statement usesAdmissible exponents for the partial Hadamard leading term

TheoremPartial Hadamard counts follow the leading term above the cubic scale#●ready to prove

The exponent \(3\) is admissible for the partial Hadamard leading term. That is, let \(N_{n,m}\) be the number of \(n \times m\) partial Hadamard matrices and let \(A_{n,4t} = 2^{4nt + (n-1)^2} (8\pi t)^{-n(n-1)/4}\) be the de Launey–Levin leading term. Then for all sequences \((n_k)\) and \((t_k)\) of natural numbers with \(n_k \ge 2\) for every \(k\) and \(t_k / n_k^3 \to \infty\) as \(k \to \infty\), the ratio \(N_{n_k, 4t_k} / A_{n_k, 4t_k}\) tends to \(1\).

theorem_wanted davisCubicAdmissible_wanted :
    IsLeadingAdmissible 3

Sources

• Davis, Counting partial Hadamard matrices in the cubic regime, arXiv:2603.30013 (2026): the leading term is asymptotic in the regime t / n³ → ∞.

Uses 1

Statement usesAdmissible exponents for the partial Hadamard leading term

TheoremNo exponent below 3 is admissible for the partial Hadamard leading term#●ready to prove

Let \(N_{n,m}\) be the number of \(n \times m\) partial Hadamard matrices and let \(A_{n,4t} = 2^{4nt + (n-1)^2} (8\pi t)^{-n(n-1)/4}\) be the de Launey–Levin leading term. Then for every real number \(\alpha < 3\) there are sequences \((n_k)\) and \((t_k)\) of natural numbers with \(n_k \ge 2\) for every \(k\) and \(t_k / n_k^{\alpha} \to \infty\) as \(k \to \infty\) along which the ratio \(N_{n_k, 4t_k} / A_{n_k, 4t_k}\) does not tend to \(1\).

theorem_wanted davisCubicSharp_wanted :
    ∀ α : ℝ, α < 3 → ¬ IsLeadingAdmissible α

Sources

• Davis (2026), same paper: a nonvanishing correction at t = Θ n³ for large fixed Θ blocks every smaller exponent for the leading term alone.

Uses 1

Statement usesAdmissible exponents for the partial Hadamard leading term

7 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.