energyCount
plain-language theorem explainer
The theorem asserts that the inductive type of molecular energy levels has exactly five elements. Researchers bounding quantum circuit depth on molecular substrates cite this to fix the energy subspace cardinality before computing total states. The proof is a direct decision procedure on the derived Fintype instance.
Claim. Let $M$ be the finite set whose elements are the electronic, vibrational, rotational, translational, and spin molecular energy levels. Then $|M|=5$.
background
The module states that a quantum circuit acting on a molecular substrate reaches a state space of cardinality $5×5=25$, which is at most $2^5=32$, so every state is reachable in at most five two-qubit gate layers. MolecularEnergyLevel is defined as an inductive type with exactly those five constructors, each deriving DecidableEq, Repr, BEq, and Fintype. The same inductive definition appears upstream in Physics.MolecularPhysicsFromRS, supplying the Fintype instance used here.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the Fintype.card expression. The tactic enumerates the five constructors of the inductive type and returns the literal equality 5.
why it matters
stateCount applies this result together with gateCount to obtain Fintype.card QuantumMolecularState = 25 and the bound $25≤2^5$. The module doc presents the claim as C4 in the Recognition Science cross-domain development, noting that a requirement for more than five gate layers per phi-rung would falsify the RS decomposition. It supplies the energy-side factor in the $5×5$ product that closes the discrete state-space argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.