Pith. sign in
module module moderate

IndisputableMonolith.Quantum.ComplexHilbertStructure

show as:
view Lean formalization →

ComplexHilbertStructure module supplies the complex Hilbert space objects that bridge Recognition Science to quantum mechanics. It imports the base HilbertSpace module and introduces sibling definitions including complex_hilbert_from_ledger and complex_hilbert_structure. The module contains only definitions and no theorems or proofs.

claimThe module defines complex Hilbert space structure over the recognition ledger together with normalized states satisfying unit norm.

background

The upstream HilbertSpace module supplies the base Hilbert space for the Recognition Science QM bridge. This module extends that foundation into the complex domain, adding structures that map ledger data to complex Hilbert spaces. Sibling declarations introduce concrete maps such as complex_hilbert_from_ledger and the normalized_state_unit_norm property.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module feeds the Recognition Science quantum mechanics bridge by supplying the complex Hilbert space layer required for subsequent quantum constructions. It sits directly after the base HilbertSpace import and precedes any quantum dynamics or measurement results.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)