substrate_healthy
plain-language theorem explainer
A substrate on Hilbert space H is healthy when there exists an instance whose Hamiltonian linear operator is self-adjoint. Workers on induced lattice gravity cite the predicate when confirming unitary evolution in their quantum models. The definition is introduced directly as an existential property over the Substrate structure with no auxiliary lemmas.
Claim. Let $H$ be a Hilbert space equipped with the RS Hilbert space structure. Then $H$ admits a healthy substrate if there exists a substrate $s$ on $H$ (consisting of a normalized state and a Hamiltonian) such that the linear operator associated to the Hamiltonian is self-adjoint.
background
The module supplies the quantum substrate for the ILG framework and links it to the quantum bridge in the Quantum directory. The Substrate structure packages a normalized state together with a Hamiltonian on any RSHilbertSpace. Upstream results include the shifted cost $H(x) = J(x) + 1$ from CostAlgebra, which converts the Recognition Composition Law into the d'Alembert equation, and the constant $A = 1$ from IntegrationGap that fixes the active edge count per tick at $D = 3$.
proof idea
The definition is a direct existential statement over the Substrate structure. It requires only that the Hamiltonian's linear operator satisfy self-adjointness; no lemmas or tactics are invoked beyond the structure fields.
why it matters
The definition supplies the predicate used by the downstream theorem substrate_ok, which asserts existence of a healthy substrate for every valid Hilbert space. It encodes the unitary-evolution requirement inside the ILG quantum bridge and aligns with the Recognition Science demand that Hamiltonians be self-adjoint. The placement closes the interface between the cost algebra and the quantum layer without invoking the phi-ladder or forcing chain explicitly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.