stateCount
The theorem shows that the quantum molecular state space, defined as the Cartesian product of the molecular energy level set and the quantum gate type set, has cardinality exactly 25. Researchers bounding quantum circuit depth on molecular substrates cite this to fix the reachable state count before invoking the five-layer gate limit. The proof is a direct term reduction that applies the product cardinality rule to the two factors whose sizes are fixed by prior results.
claimThe cardinality of the Cartesian product of the set of molecular energy levels and the set of quantum gate types equals 25, i.e., $|$MolecularEnergyLevel$|$ $×$ $|$QuantumGateType$|$ $= 25$.
background
The CrossDomain.QuantumMolecularBound module defines the quantum molecular state space as the product type MolecularEnergyLevel × QuantumGateType. Two upstream theorems establish that the cardinality of MolecularEnergyLevel equals 5 and the cardinality of QuantumGateType equals 5. This local setting supports the structural claim that the reachable state space has cardinality 25, which satisfies 25 ≤ 2^5 = 32 and therefore fits inside five gate layers.
proof idea
The proof is a one-line wrapper that invokes simplification on the product definition of QuantumMolecularState together with the general rule for the cardinality of a product and the two cardinality theorems energyCount and gateCount.
why it matters in Recognition Science
This theorem supplies the state_count field inside the quantumMolecularBoundCert certificate. It realizes the core structural claim of the module's C4 section, confirming that the 25-state space lies inside the five-layer bound required by the Recognition Science decomposition. The result aligns with the eight-tick octave by ensuring molecular targets fit the 2^3 period structure.
scope and limits
- Does not define the internal elements of MolecularEnergyLevel or QuantumGateType.
- Does not prove that every one of the 25 states is physically realizable.
- Does not derive the five-layer bound from the J-function or phi-ladder.
- Does not address continuous or higher-dimensional state spaces.
Lean usage
state_count := stateCountformal statement (Lean)
35theorem stateCount : Fintype.card QuantumMolecularState = 25 := by
proof body
Term-mode proof.
36 simp only [QuantumMolecularState, Fintype.card_prod, energyCount, gateCount]
37
38/-- 2⁵ = 32 ≥ 25. So ceil(log₂ 25) ≤ 5. -/