Degrees of freedom $K$ from a signature $x=(x_1,x_2,\dots)$

Definition

hardy2001_signature

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

combinatoricsmathematical-physicsquantum-foundations

For a list of natural numbers $x=(x_1,\dots,x_L)$ , the signature of a probability theory, and a dimension $N\in\mathbb N$ , the number of degrees of freedom is

K_x(N)=Nx_1+\frac1{2!}N(N-1)x_2+\frac1{3!}N(N-1)(N-2)x_3+\cdots=\sum_{k=1}^{L}\binom Nk\,x_k .

Hardy counts one degree of freedom $x_1$ for each one-dimensional subspace spanned by basis states, $x_2$ further degrees of freedom for each two-dimensional subspace, $x_3$ for each three-dimensional subspace, and so on. Classical probability theory has signature $(1,0,0,\dots)$ and complex quantum theory has $(1,2,0,\dots)$ .

Formalization Note The signature is a finite list [x₁, …, x_L], and all later entries are understood to be $0$ . The coefficient $\frac1{k!}N(N-1)\cdots(N-k+1)$ is written as the binomial coefficient $\binom Nk$ . It is equal to it for every natural $N$ , including $N<k$ , where both vanish.

Definition code

import Mathlib

namespace HardyFiveAxioms

/-- Number of degrees of freedom `K` determined by a signature `x = (x₁, x₂, …)` for a system
of dimension `N` (Hardy 2001, Eq. (28)):
`K = N x₁ + (1/2!) N(N-1) x₂ + (1/3!) N(N-1)(N-2) x₃ + ⋯ = ∑ₖ (N choose k) xₖ`.
The signature is given as the finite list `[x₁, x₂, …, x_L]`; entries beyond `L` are zero. -/
def dofOfSignature (x : List ℕ) (N : ℕ) : ℕ :=
  ∑ i : Fin x.length, N.choose (i.val + 1) * x.get i

end HardyFiveAxioms

Source

L. Hardy, *Quantum Theory From Five Reasonable Axioms*, arXiv:quant-ph/0101012v4 (2001), https://arxiv.org/abs/quant-ph/0101012, p. 8, Section 5, Eq. (28)

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 a finite list $x=(x_1,\dots,x_L)$ of natural numbers ( $L$ is the length of the list, possibly $0$ ) and a natural number $N$ , the natural number $K_x(N)$ is defined as

K_x(N)=\sum_{i=0}^{L-1}\binom{N}{i+1}\,x_{i+1}=\sum_{k=1}^{L}\binom Nk x_k ,

where $\binom Nk$ is the usual binomial coefficient, equal to $0$ when $k>N$ . For the empty list $K_x(N)=0$ , and for $N=0$ every term vanishes, so $K_x(0)=0$ . Everything is computed in $\mathbb N$ , so there is no division and no truncation.

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

Degrees of freedom KKK from a signature x=(x1,x2,… )x=(x_1,x_2,\dots)x=(x1​,x2​,…)

Degrees of freedom $K$ from a signature $x=(x_1,x_2,\dots)$