QuantumOpticalState
plain-language theorem explainer
QuantumOpticalState enumerates the five canonical states of light in the Recognition Science treatment of quantum optics. Researchers deriving photon statistics from the recognition lattice would cite it to fix the discrete state space before applying J-cost calculations. The declaration is a direct inductive enumeration that derives Fintype automatically, which immediately supports the downstream cardinality result of exactly five states.
Claim. The set of quantum optical states is the finite collection consisting of Fock states, coherent states, squeezed states, thermal states, and entangled states, with cardinality 5.
background
In Recognition Science, photons are recognition bosons on the electromagnetic lattice. Quantum optics is modeled by five canonical states that realize configuration dimension D = 5. The coherent state is defined to carry J-cost zero, corresponding to classical light at recognition equilibrium, while the remaining states carry positive J-cost.
proof idea
The declaration is a direct inductive definition introducing five constructors. Derivation of Fintype, DecidableEq, Repr, and BEq is automatic via the deriving clause, with no explicit proof steps required.
why it matters
This definition supplies the state space used by the cardinality theorem quantumOpticalCount and the certification structure QuantumOpticsCert. It realizes the framework claim that five states suffice for quantum optics and aligns with the J-uniqueness property from the forcing chain. The coherent-zero clause in the downstream certificate directly references the J-cost definition from the Cost module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.