energy_surj
plain-language theorem explainer
The projection from quantum molecular states onto molecular energy levels is surjective. Researchers bounding quantum circuit depth for molecular targets cite this to confirm every discrete energy level is attainable inside the 25-state space. The proof is a one-line wrapper that supplies an explicit preimage pair for any target energy level.
Claim. The function mapping each pair (molecular energy level, quantum gate type) to its molecular energy level is surjective.
background
The module defines the quantum molecular state space as the Cartesian product of discrete molecular energy levels and a five-element set of quantum gate types (Pauli, Clifford, T-gate, CNOT, Toffoli). This product yields cardinality 25, satisfying the inequality 2^5 >= 25 and thereby ensuring reachability in at most five two-qubit gate layers. The local setting is the cross-domain structural claim that any quantum circuit acting on a molecular substrate stays inside this finite space, with the bound declared sharp.
proof idea
The proof is a one-line wrapper. It applies intro to the surjectivity goal and constructs the witness state as the pair consisting of the target energy level together with the Pauli gate, using reflexivity to match the projection.
why it matters
This result populates the energy_surj field inside the QuantumMolecularBoundCert structure, which certifies both the state count of 25 and the five-layer bound. It supports the cross-domain verification that the decomposition into energy levels and gate types is exhaustive, aligning with the Recognition Science requirement that molecular targets fit inside the eight-tick octave without exceeding five layers per phi-rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.