quantumMolecularBoundCert
plain-language theorem explainer
This definition constructs the certificate structure for the quantum molecular bound by assembling five component results into a single record. Researchers modeling quantum circuits on molecular substrates would cite it to verify that exactly 25 states are reachable with at most five gate layers. The construction is a direct field assignment that references the state-count theorem, the power-of-two bound, the logarithm identity, and the two surjectivity lemmas.
Claim. The quantum molecular bound certificate asserts that the cardinality of the product state space is 25, that $2^5 >= 25$, that ceil(log base 2 of 25) equals 5, and that the projections from states onto the five energy levels and five gate types are both surjective.
background
The module establishes a cross-domain bound for quantum circuits acting on molecular substrates. QuantumMolecularState is defined as the Cartesian product of MolecularEnergyLevel (five discrete levels) and QuantumGateType (five gate families), so its cardinality is the product of the two counts. The certificate structure QuantumMolecularBoundCert packages four numerical claims and two surjectivity statements that together certify the 5-by-5 state space is covered by five layers of two-qubit gates.
proof idea
The definition is a one-line wrapper that populates the five fields of QuantumMolecularBoundCert by direct reference to the sibling theorems stateCount, fiveLayerBound, log25_eq_5, energy_surj, and gate_surj. No additional tactics or reductions are performed; the proof body simply supplies the already-proved values for each field.
why it matters
The declaration supplies the single packaged certificate required by the C4 structural claim in the module documentation. It confirms that the 25-state space satisfies the layer bound ceil(log2 25) = 5, which is presented as a sharp test: any molecular target needing more than five layers per phi-rung would falsify the RS decomposition. No downstream uses are recorded yet, leaving the certificate available for later cross-domain arguments that invoke the five-layer sufficiency.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.