Hardy's degrees of freedom: $K(N)=N^r$ for a positive integer $r$

Proved

HardyFiveAxioms.dof_eq_pow

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

mathematical-physicsnumber-theoryquantum-foundations

Let $K$ assign to every dimension $N=1,2,3,\dots$ a number of degrees of freedom $K(N)\in\mathbb N$ . Suppose that

$K(N+1)\ge K(N)+1$ for every $N\ge1$ , which Hardy derives from the subspace axiom (Axiom 3);
$K(N_AN_B)=K(N_A)\,K(N_B)$ for all $N_A,N_B\ge1$ , which is the composite-systems axiom (Axiom 4).

Then there is a positive integer $r$ such that

K(N)=N^r\qquad\text{for all }N\ge1 .

This is Eq. (57) of the paper. Together with Section 8.5, which rules out $r=1$ by the continuity axiom, and the simplicity axiom, it yields $K=N^2$ , the quantum value.

Formalization Note $K$ is a function ℕ → ℕ. Its value at $N=0$ is unconstrained and irrelevant. The paper's standing fact $K\ge1$ is not assumed, because it follows from the two hypotheses.

Preamble

import Mathlib

Formal statement

namespace HardyFiveAxioms

/-- Hardy 2001, Section 8.1, Eq. (57): if the number of degrees of freedom `K(N)` satisfies
`K(N+1) ≥ K(N) + 1` (consequence of the subspace axiom) and `K(N_A N_B) = K(N_A) K(N_B)`
(composite systems axiom), then `K(N) = N^r` for a positive integer `r`. -/
theorem dof_eq_pow (K : ℕ → ℕ)
    (hinc : ∀ N : ℕ, 1 ≤ N → K N + 1 ≤ K (N + 1))
    (hmul : ∀ NA NB : ℕ, 1 ≤ NA → 1 ≤ NB → K (NA * NB) = K NA * K NB) :
    ∃ r : ℕ, 1 ≤ r ∧ ∀ N : ℕ, 1 ≤ N → K N = N ^ r := 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. 16, Section 8.1, Eqs. (56)–(57) (with Appendix 2, pp. 29–30)

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.

Let $K:\mathbb N\to\mathbb N$ be any function. Assume:

for every natural number $N\ge1$ , $K(N)+1\le K(N+1)$ ;
for all natural numbers $N_A\ge1$ and $N_B\ge1$ , $K(N_A\cdot N_B)=K(N_A)\cdot K(N_B)$ .

Then there exists a natural number $r$ with $r\ge1$ such that

K(N)=N^r\quad\text{for every natural number }N\ge1 .

Nothing is assumed or concluded about $K(0)$ . Hypothesis 1 makes $K$ strictly increasing on $\{1,2,\dots\}$ . Both hypotheses are satisfiable, e.g. by $K(N)=N^r$ for any $r\ge1$ .

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

Hardy's degrees of freedom: K(N)=NrK(N)=N^rK(N)=Nr for a positive integer rrr

Hardy's degrees of freedom: $K(N)=N^r$ for a positive integer $r$