Substrate
plain-language theorem explainer
The Substrate structure packages a normalized state vector together with a bounded-below Hamiltonian operator inside an RS Hilbert space. Experimental modules that treat dark matter as a substrate effect rather than particles cite this packaging to derive null WIMP predictions and galaxy diversity results. The declaration is a direct structure definition carrying no proof obligations or computational content.
Claim. A substrate in an RS Hilbert space $H$ consists of a normalized state vector $ψ$ satisfying $‖ψ‖=1$ together with a Hamiltonian operator $Ĥ$ whose expectation values are bounded below by some real $E_0$.
background
The module supplies the quantum substrate for the Induced Lattice Gravity framework and links it to the Quantum Bridge defined in the Quantum namespace. An RS Hilbert space is a separable complex Hilbert space that is complete and carries a seminormed additive group structure. NormalizedState requires a vector of unit norm. Hamiltonian extends an observable with the explicit lower bound condition on real parts of expectation values. Upstream, the shifted cost function $H(x)=J(x)+1$ converts the Recognition Composition Law into the d'Alembert wave equation.
proof idea
The declaration is a structure definition that directly introduces the two fields state of type NormalizedState H and hamiltonian of type Hamiltonian H. No lemmas are invoked and no tactics are executed; the construction is purely data packaging.
why it matters
This definition supplies the substrate model invoked by the EA-005 and EA-011 experimental certificates, which conclude that direct detection experiments must return null signals and that ultra-diffuse galaxy mass ratios arise from spatial variation in substrate coherence. It realizes the quantum interface required by the ILG framework inside Recognition Science, where the Hilbert space carries the cost algebra and the eight-tick octave structure. The structure closes the bridge between algebraic cost functionals and observable quantum mechanics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.