pith. sign in
module module high

IndisputableMonolith.Quantum.Observables

show as:
view Lean formalization →

This module defines quantum observables as self-adjoint operators on Hilbert spaces in the Recognition Science QM bridge. It supplies the basic types used by commutation and ILG modules. The content consists of type declarations and sibling definitions for Observable, Projector, and Hamiltonian with no proofs.

claimAn observable is a self-adjoint operator $A$ on Hilbert space $H$ with $A^* = A$. Projectors are idempotent self-adjoint operators and the Hamiltonian is the generator of time evolution.

background

The module sits inside the quantum domain and imports the Hilbert space construction whose doc-comment reads '# Hilbert Space for Recognition Science QM Bridge'. It uses the inner-product and adjoint infrastructure from Mathlib to formalize self-adjointness. Sibling declarations introduce Observable, Projector, and Hamiltonian as the core objects.

proof idea

this is a definition module, no proofs

why it matters in Recognition Science

The module supplies the observable definitions that feed the CommutationStructure module (whose doc states 'Structural commutation content: projector algebra is idempotent') and the ILG.Substrate module (whose doc states 'This module connects the ILG framework to the proper Quantum Bridge'). It therefore anchors the quantum side of the Recognition Science bridge to induced lattice gravity.

scope and limits

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (3)