Quantum Observables

Observables and the bridge

In quantum mechanics, an observable is a measurable physical quantity, such as position, momentum, or energy. The mathematical object that represents an observable is a self-adjoint operator on a Hilbert space, a linear map that equals its own adjoint. This condition guarantees that the possible measurement outcomes, the eigenvalues, are real numbers. The framework defines observables in exactly this classical way, then adds a structure for the special case of a Hamiltonian, the operator whose eigenvalues are the allowed energy levels.

The framework defines an observable as a bounded linear operator with the self-adjoint condition. A projection operator is an observable that is idempotent, meaning applying it twice gives the same result as applying it once; these correspond to yes-no questions about a system. The Hamiltonian extends the observable structure with a bounded-below condition: there exists a real number E₀ such that the expectation value of the energy is always at least E₀. This captures the physical requirement that energy cannot be arbitrarily negative.

In Recognition Science, the ledger, a discrete record of recognition events, provides the underlying structure. The framework builds the bridge from that ledger to standard quantum mechanics by defining these operators on an RSHilbertSpace, a Hilbert space equipped with the framework's structure. This means the framework does not discard the conventional mathematical apparatus; it re-derives the definitions within its own setting. The framework establishes that the standard objects of quantum theory, observables, projectors, and Hamiltonians, can be expressed in the framework's language.

The practical consequence is that the framework can now state and prove theorems about quantum systems using its own foundations. The Hamiltonian's bounded-below condition is a theorem-ready statement: it gives a concrete property that any energy operator must satisfy. This sets the stage for further results about spectra and dynamics, all grounded in the same forcing chain that produces the framework's constants and dimensions.

/-- Self-adjoint operator (observable) -/
structure Observable (H : Type*) [RSHilbertSpace H] where
  /-- Bounded linear operator -/
  op : H →L[ℂ] H
  /-- Self-adjoint condition -/
  self_adjoint : ∀ x y : H, ⟪op x, y⟫_ℂ = ⟪x, op y⟫_ℂ

/-- Projection operator -/
structure Projector (H : Type*) [RSHilbertSpace H] extends Observable H where
  /-- Idempotent property -/
  idempotent : op.comp op = op

/-- Hamiltonian operator -/
structure Hamiltonian (H : Type*) [RSHilbertSpace H] extends Observable H where
  /-- Energy must be bounded below -/
  bounded_below : ∃ E₀ : ℝ, ∀ ψ : NormalizedState H,
    (⟪op ψ.vec, ψ.vec⟫_ℂ).re ≥ E₀

What this page does not claim

The framework does not prove that any specific physical system has a Hamiltonian. This does not establish that the framework's observables reproduce all of quantum mechanics. The self-adjoint condition here is assumed, not derived 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/Observables.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: