pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Quantum.Observables

show as:
view Lean formalization →

The Observables module supplies the basic definitions for quantum observables in the Recognition Science framework. It declares Observable as a self-adjoint operator on the Hilbert space, along with Projector and Hamiltonian structures. This module is imported by the commutation algebra and the ILG substrate. It contains only definitions, drawing on Mathlib's adjoint and inner product machinery for the self-adjoint condition.

claimLet $H$ be the Hilbert space from the Recognition Science QM bridge. An observable is a self-adjoint operator $A: H → H$ with $A^* = A$. A projector is an idempotent self-adjoint operator $P$ satisfying $P^2 = P = P^*$. The Hamiltonian is the observable generating time evolution.

background

This module sits in the Quantum domain and imports the HilbertSpace module, which establishes the inner product space for the QM formalization in Recognition Science. It defines the primary objects used in measurement theory: observables as self-adjoint operators, projectors as idempotent observables, and the Hamiltonian as the energy observable. The setting assumes the standard axioms of Hilbert space quantum mechanics adapted to the Recognition Science constants.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The definitions here are used directly in the CommutationStructure module to establish projector idempotence and in the ILG.Substrate module to link the quantum bridge to induced lattice gravity. It fills the foundational layer for observables in the quantum-relativity interface of the Recognition framework.

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)