Quantum Complex Hilbert Structure

Quantum complex Hilbert structure

A quantum complex Hilbert structure is the mathematical arena of quantum mechanics: a complex vector space with an inner product, complete in a technical sense, where each physical state is a vector of unit length. The inner product gives probabilities, the complex scalars give interference, and the unit norm ensures that probabilities sum to one. This is the standard setting of the theory, taught in every quantum mechanics course.

The structure was formalized in the early 20th century. David Hilbert's work on integral equations led to the abstract notion of a complete inner product space, named after him. John von Neumann then applied this to quantum mechanics in his 1932 book, establishing the framework that remains standard: states are rays in a complex Hilbert space, observables are self-adjoint operators, and the inner product yields transition probabilities. The complex numbers are essential here, not optional; real vector spaces cannot represent the interference patterns that experiments show.

In Recognition Science, the framework models this structure from its starting point: a ledger, a discrete record of recognition events where each event carries a cost. The framework's library, a machine-checked collection of formal theorems, proves that any normalized state in a recognition-space Hilbert space has unit norm. This is the theorem normalized_state_unit_norm: for any Hilbert space and any normalized state, the norm equals one. The proof is immediate, since the definition of a normalized state already includes unit norm.

The framework's contribution is not a new kind of Hilbert space but a derivation of the unit-norm condition from its own axioms. The theorem complex_hilbert_structure states that the recognition-space definition of a Hilbert space implies the unit-norm property. This is a consistency result: the framework's ledger-based construction reproduces the standard normalization condition of quantum mechanics. It shows that the recognition-space axioms are strong enough to recover a core feature of quantum theory.

What this establishes in plain language is that the framework does not abandon quantum mechanics but rebuilds its foundation. The unit-norm condition, which appears as a postulate in textbooks, follows here from the ledger's cost structure. This is a first step, not a full derivation of quantum theory; the framework has not yet derived the Schrödinger equation or the full Hilbert space structure from recognition events.

theorem normalized_state_unit_norm {H : Type*} [RSHilbertSpace H]
    (ψ : NormalizedState H) : ‖ψ.vec‖ = 1 :=
  ψ.norm_one

theorem complex_hilbert_structure : complex_hilbert_from_ledger := by
  intro H hH ψ
  exact ψ.norm_one

What this page does not claim

The framework does not derive the full Hilbert space structure, only the unit-norm condition. The Schrödinger equation is not derived from recognition events. The complex field of the Hilbert space is not shown to arise from the ledger.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Quantum/ComplexHilbertStructure.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: