Hamiltonian
plain-language theorem explainer
The Hamiltonian structure extends Observable to require that the real part of the expectation value is bounded below on all normalized states. Researchers building the Recognition Science quantum bridge would cite it when passing from cost functionals to energy operators. The declaration is a direct structure extension that adds one predicate to the self-adjoint operator.
Claim. A Hamiltonian on a Hilbert space $H$ equipped with the Recognition Science structure is a self-adjoint bounded linear operator $op$ such that there exists $E_0$ with $Re⟨op ψ, ψ⟩ ≥ E_0$ for every normalized state $ψ$.
background
In the Observable Algebra module for the Recognition Science QM bridge, observables are self-adjoint operators on an RSHilbertSpace. The sibling Observable structure packages a bounded linear operator op together with the adjointness condition ⟨op x, y⟩ = ⟨x, op y⟩. NormalizedState supplies unit vectors so that expectation values are well-defined. Upstream CostAlgebra.H reparametrizes the J-cost via H(x) = J(x) + 1, supplying the algebraic source of energy-like quantities; the same H appears in the Cost.FunctionalEquation module.
proof idea
This is a structure definition that extends Observable and adds the single field bounded_below. No lemmas or tactics are invoked; the declaration simply records the operator and the lower-bound predicate on normalized states.
why it matters
The structure supplies the quantum energy operator used by EnergyConservationCert, hamiltonian_status, and the Noether theorems in the Action module. It realizes the energy observable required after the T5 J-uniqueness step and the shift to the H-cost, completing the passage from classical cost algebra to quantum mechanics. It touches the open question of deriving explicit spectra from the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.