Signatures of real, quaternionic and $K=N^3$ theories

Proved

HardyFiveAxioms.signature_real_quaternionic_cubic

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

combinatoricsmathematical-physicsquantum-foundations

For every $N\in\mathbb N$ :

the real-Hilbert-space signature $(1,1,0,\dots)$ gives $K=N+\binom N2=\tfrac12N(N+1)$ ;
the quaternionic signature $(1,4,0,\dots)$ gives $K=N+4\binom N2=2N^2-N$ ;
the signature $(1,6,6,0,\dots)$ gives $K=N+6\binom N2+6\binom N3=N^3$ .

In Lean these read $2K_{(1,1)}(N)=N(N+1)$ , $K_{(1,4)}(N)+N=2N^2$ and $K_{(1,6,6)}(N)=N^3$ .

Formalization Note The forms $2K=N(N+1)$ and $K+N=2N^2$ avoid natural-number division and subtraction.

Preamble

import Mathlib
import Definitions.Def_hardy2001_signature

Formal statement

namespace HardyFiveAxioms

/-- Hardy 2001, Sections 5 and 8.1: the real-Hilbert-space signature `(1, 1, 0, …)` gives
`K = N(N+1)/2`, the quaternionic signature `(1, 4, 0, …)` gives `K = 2N² - N`, and the
signature `(1, 6, 6, 0, …)` gives `K = N³`. -/
theorem signature_real_quaternionic_cubic (N : ℕ) :
    2 * dofOfSignature [1, 1] N = N * (N + 1) ∧
      dofOfSignature [1, 4] N + N = 2 * N ^ 2 ∧
      dofOfSignature [1, 6, 6] N = N ^ 3 := 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. 8, Section 5 (after Eq. (28)); p. 17, Section 8.1 (real and quaternionic Hilbert spaces,

K=N^3

)

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 every natural number $N$ , all in $\mathbb N$ :

$2\big(\binom N1+\binom N2\big)=N(N+1)$ ;
$\binom N1+4\binom N2+N=2N^2$ ;
$\binom N1+6\binom N2+6\binom N3=N^3$ .

Here the left-hand sums are $K_{[1,1]}(N)$ , $K_{[1,4]}(N)$ and $K_{[1,6,6]}(N)$ for the signature function of hardy2001_signature.

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

Signatures of real, quaternionic and K=N3K=N^3K=N3 theories

Signatures of real, quaternionic and $K=N^3$ theories