quantumOpticalCount
plain-language theorem explainer
The theorem establishes that the inductive type of canonical quantum optical states in Recognition Science has cardinality exactly five. Researchers deriving quantum optics from the recognition lattice would cite this to fix the dimension of the state space at configDim D = 5. The proof is a one-line decision procedure that exhausts the five constructors of the finite type.
Claim. Let $S$ be the set of canonical quantum optical states consisting of the Fock, coherent, squeezed, thermal, and entangled states. Then $|S| = 5$.
background
The module Quantum Optics from RS defines an inductive type QuantumOpticalState with exactly five constructors: fock, coherent, squeezed, thermal, entangled, deriving Fintype, DecidableEq, and Repr. The module doc states that these five states equal configDim D = 5 on the EM recognition lattice, with the coherent state identified as the J = 0 classical limit. The upstream inductive definition supplies the finite-type structure used by the cardinality claim.
proof idea
The proof is a one-line wrapper that invokes the decide tactic to compute the cardinality of the finite inductive type QuantumOpticalState by enumerating its five constructors.
why it matters
This supplies the five_states field inside the quantumOpticsCert definition that certifies the quantum optics construction. It fills the B14/B16 claim that photon states on the EM recognition lattice yield exactly five configurations. The result anchors the emergence of quantum optics from the J-cost function and recognition composition law, consistent with the five-state span of configDim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.