Real Hilbert spaces: composites have more than $K_AK_B$ degrees of freedom

Proved

HardyFiveAxioms.real_composite_excess

by Lucas · Oct 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsmathematical-physicsquantum-foundations

Let $K_{\mathbb R}(N)=N+\binom N2=\tfrac12N(N+1)$ be the number of degrees of freedom of real-Hilbert-space quantum theory, i.e. signature $(1,1,0,\dots)$ . For all $N_A,N_B\ge2$ ,

K_{\mathbb R}(N_A)\,K_{\mathbb R}(N_B)<K_{\mathbb R}(N_AN_B).

So real quantum theory violates $K=K_AK_B$ of Axiom 4: some degrees of freedom of a composite can only be measured jointly.

Formalization Note For $N_A=1$ or $N_B=1$ equality holds, which is why both dimensions are taken $\ge2$ .

Preamble

import Mathlib
import Definitions.Def_hardy2001_signature

Formal statement

namespace HardyFiveAxioms

/-- Hardy 2001, Section 8.1: for real Hilbert spaces (signature `(1, 1, 0, …)`), a composite
system has more degrees of freedom than the product of those of its subsystems. -/
theorem real_composite_excess (NA NB : ℕ) (hA : 2 ≤ NA) (hB : 2 ≤ NB) :
    dofOfSignature [1, 1] NA * dofOfSignature [1, 1] NB < dofOfSignature [1, 1] (NA * NB) := by sorry

end HardyFiveAxioms

Source

L. Hardy, *Quantum Theory From Five Reasonable Axioms*, arXiv:quant-ph/0101012v4 (2001), https://arxiv.org/abs/quant-ph/0101012, p. 17, Section 8.1, paragraph on real Hilbert spaces

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic)

NON-BLIND READ-BACK — NOT INDEPENDENT TESTIMONY. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statement below, with full knowledge of the source paper and of the intended meaning. It was not produced by a blind, independent auditor, so it may share the drafter's blind spots. Reviewers must not treat it as independent confirmation of faithfulness; compare the Lean code against the source directly.

For natural numbers $N_A\ge2$ and $N_B\ge2$ , writing $K(N)=\binom N1+\binom N2$ (the signature function for $[1,1]$ ):

K(N_A)\cdot K(N_B)<K(N_A\cdot N_B),

a strict inequality of natural numbers.

Human review

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

View graph

Real Hilbert spaces: composites have more than KAKBK_AK_BKA​KB​ degrees of freedom

Real Hilbert spaces: composites have more than $K_AK_B$ degrees of freedom