QuantumMolecularDepthCert
plain-language theorem explainer
The certificate structure records that the RS-derived count of molecular quantum state classes equals 25, which fits within 5-bit addressing but exceeds 4 bits. Researchers working on quantum molecular design bounds in the Recognition Science framework cite this when establishing minimal addressing depth for state preparation. It packages three arithmetic facts drawn from the product of five energy levels and five gate types.
Claim. Let $N$ be the number of molecular quantum state classes, defined as the product of the cardinality of molecular energy levels and the cardinality of quantum gate types. The certificate asserts $N=25$, $N≤2^5$, and $2^4<N$.
background
In the C4 module the Recognition Science framework counts preparable molecular states as the product of five molecular energy levels and five quantum gate types. This product is formalized as the definition molecularQuantumStateClasses := Fintype.card MolecularEnergyLevel * Fintype.card QuantumGateType, which evaluates to 25 and fixes the minimal bit depth needed to index all RS-preparable classes.
proof idea
The structure is assembled by directly asserting the three fields: equality to 25, the inequality ≤ 2^5, and the strict inequality > 2^4. No lemmas or tactics are invoked inside the structure; the facts stand as record fields.
why it matters
This certificate supplies the Lean-verified counting foundation for the C4 claim, feeding directly into the downstream quantumMolecularDepthCert construction. It marks the formal, machine-checked portion of the design-depth argument while leaving the stronger physical claim of reaching a specific target in five two-qubit layers as an empirical question.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.