quantumMolecularDepthCert
plain-language theorem explainer
quantumMolecularDepthCert assembles a record that certifies exactly 25 molecular quantum state classes exist, that five bits suffice to address them, and that four bits do not. A researcher working on quantum molecular design bounds in Recognition Science would cite it to anchor the addressing-depth claim. The definition is a direct structure literal that substitutes three upstream theorems for the three fields of QuantumMolecularDepthCert.
Claim. Let $N$ denote the number of molecular quantum state classes formed as the product of molecular energy levels and quantum gate types. Then $N=25$, $N≤2^5$, and $2^4<N$.
background
Module C4 treats quantum molecular design depth inside the Recognition Science framework. It defines molecularQuantumStateClasses as the product of molecularEnergyCount and quantumGateTypeCount, which evaluates to 25 prepared state classes. The structure QuantumMolecularDepthCert packages the three properties: exact equality to 25, addressability by five bits (≤32), and strict inequality over four bits (>16).
proof idea
The definition constructs an instance of QuantumMolecularDepthCert by direct field assignment: state_classes_25 receives molecularQuantumStateClasses_25, addressable_by_five_bits receives molecularQuantumStateClasses_le_2pow5, and not_addressable_by_four_bits receives twoPowerFour_lt_stateClasses.
why it matters
This supplies the Lean-certified counting foundation for the C4 claim on quantum molecular design depth. It confirms that five bits index all RS-preparable classes arising from five energy levels and five gate types, consistent with the eight-tick octave structure (T7) of Recognition Science. No downstream theorems yet consume the certificate, leaving open the algorithmic question of concrete target reachability in five two-qubit layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.