twoPowerFour_lt_stateClasses
The theorem proves that the number of RS-preparable molecular quantum state classes exceeds 16. Researchers certifying minimal addressing depth in quantum molecular design cite it to show four bits cannot index all states. The proof substitutes the explicit count of 25 and reduces the inequality by numerical normalization.
claim$2^4 < Fintype.card(MolecularEnergyLevel) × Fintype.card(QuantumGateType)$, where the product equals the number of prepared state classes.
background
The C4 module defines prepared state classes as the product of five molecular energy levels and five quantum gate types. The definition molecularQuantumStateClasses computes this cardinality directly as Fintype.card MolecularEnergyLevel * Fintype.card QuantumGateType. An upstream theorem establishes that this product equals exactly 25, providing the concrete count used for bit-depth arguments. The module states that five bits suffice to index the full set while the stronger claim of reaching specific targets in five two-qubit layers remains empirical.
proof idea
One-line wrapper that rewrites via the equality molecularQuantumStateClasses_25 and applies norm_num to confirm 16 < 25.
why it matters in Recognition Science
The result supplies the not_addressable_by_four_bits field inside the quantumMolecularDepthCert definition. It completes the C4 counting step that confirms a 5-bit depth is the minimal addressable size for the 25 classes. This sits inside the Recognition Science derivation of quantum computing depth, where the product of energy levels and gate types sets the state-class yardstick.
scope and limits
- Does not prove that any concrete molecule reaches a target state in five layers.
- Does not incorporate decoherence, error rates, or physical gate fidelities.
- Does not extend the bound to systems with more than five energy levels or gate types.
- Does not address the algorithmic search cost of selecting the correct sequence.
Lean usage
example : 2 ^ 4 < molecularQuantumStateClasses := twoPowerFour_lt_stateClassesformal statement (Lean)
39theorem twoPowerFour_lt_stateClasses :
40 2 ^ 4 < molecularQuantumStateClasses := by
proof body
Term-mode proof.
41 rw [molecularQuantumStateClasses_25]
42 norm_num
43