gate_surj
plain-language theorem explainer
The gate-type projection on pairs of molecular energy levels and gate types is surjective. Researchers bounding quantum-circuit depth for molecular substrates cite the result to confirm every gate type appears in the 25-state space. The proof is a one-line wrapper that supplies the electronic energy level as a preimage for any target gate type.
Claim. The projection map sending each pair $(e, g)$ with $e$ a molecular energy level and $g$ a quantum gate type to $g$ is surjective.
background
The module defines the reachable state space as the product MolecularEnergyLevel × QuantumGateType. MolecularEnergyLevel is the inductive type whose five constructors are electronic, vibrational, rotational, translational and spin. The product therefore contains exactly 25 elements, and the surrounding claim is that this cardinality is covered by a circuit of depth at most five (since 2^5 = 32).
proof idea
The proof is a one-line wrapper. It applies intro to the surjectivity goal and then exhibits the explicit preimage pair consisting of the electronic constructor paired with the arbitrary target gate type, followed by reflexivity.
why it matters
The theorem supplies the gate-surjectivity field required by the QuantumMolecularBoundCert structure. That certificate in turn verifies the 5-layer bound asserted in the module header for the 25-state space. The result therefore closes one half of the structural claim that every combination of energy level and gate type is reachable inside the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.