QuantumMolecularBoundCert
plain-language theorem explainer
The structure certifies that the quantum molecular state space has cardinality 25 as the product of five molecular energy levels and five quantum gate types, with the inequality 2^5 >= 25 and log2(25) + 1 = 5 establishing a five-layer gate bound. Circuit theorists bounding depth for molecular simulations would cite the certificate to confirm reachability within five layers. It is assembled as a direct packaging of pre-proven surjectivity results for the two projections together with the cardinality and inequality facts.
Claim. Let $M$ be the set of molecular energy levels and $G$ the set of quantum gate types. Let $S := M × G$. Then $|S| = 25$, $2^5 ≥ 25$, $log_2 25 + 1 = 5$, the projection $S → M$ is surjective, and the projection $S → G$ is surjective.
background
The module defines the state space as the Cartesian product QuantumMolecularState := MolecularEnergyLevel × QuantumGateType. It asserts that this product yields exactly 25 states and that five two-qubit gate layers suffice because 2^5 = 32 exceeds 25, with the ceiling of log2(25) equal to 5. Upstream results supply the two surjectivity theorems: energy_surj proves the first projection is onto by pairing any energy level with a fixed Pauli gate, while gate_surj proves the second projection is onto by pairing any gate type with a fixed electronic energy level.
proof idea
As a structure definition with an empty proof body, the declaration simply assembles five fields: the cardinality equality stateCount, the inequality fiveLayerBound, the logarithm identity log25_eq_5, and the two surjectivity theorems energy_surj and gate_surj. No tactics or reductions occur inside the declaration.
why it matters
The certificate is instantiated by the downstream definition quantumMolecularBoundCert, which supplies the concrete values for use in cross-domain arguments. It realizes the C4 structural claim that 5 × 5 = 25 states remain reachable in at most five layers, providing a sharp bound whose violation would falsify the RS decomposition for molecular targets. The five-layer figure aligns with the framework's emphasis on small integer layer counts but remains specialized to this 25-state space rather than deriving directly from the eight-tick octave or phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.