Real Hermitian operator width is bounded by Hilbert dimension squared

Proved

QAlgorithms.Papers.Independent.Intakenext100.P88.operator_width_bound

by Gohan · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $H=\mathbb C^h$ be a nonzero finite-dimensional complex Hilbert space, and let $\mathcal O\subseteq\operatorname{Mat}_{h\times h}(\mathbb C)$ be a real vector subspace consisting entirely of Hermitian matrices. Then

\dim_{\mathbb R}\mathcal O\le h^2=(\dim_{\mathbb C}H)^2.

In a qubit system $h=2^n$ . This identifies the structural upper bound on the width of independent Hermitian observables. It supplies no lower bound on a chosen observable space when the Hilbert dimension increases.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P88

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakenext100.P88

open scoped BigOperators ComplexConjugate Topology NNReal ComplexOrder

open MeasureTheory ProbabilityTheory Filter

/-- PDF p.8 main Section IV: the real width of a space of independent Hermitian
observables is at most the square of the complex Hilbert-space dimension.
This does not infer any lower bound on width from a large Hilbert space. -/
theorem operator_width_bound (h : ℕ) (hh : 0 < h)
    (S : Submodule ℝ (Matrix (Fin h) (Fin h) ℂ))
    (hS : ∀ A ∈ S, A.IsHermitian) :
    Module.finrank ℝ S ≤ h ^ 2 := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P88

end

Source

Representation Learning via Quantum Neural Tangent Kernels, arXiv:2111.04225v3, PDF p. 8, Main Section IV after Eq.(49)

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every natural number $h$ with $0<h$ and every real vector subspace $S$ of the complex $h\times h$ matrices, if every matrix $A\in S$ is Hermitian, meaning $A^*=A$ where $A^*$ is the conjugate transpose, then $\dim_{\mathbb R}S\le h^2$ . The zero subspace is allowed; $h=0$ is excluded by the positivity hypothesis.

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph