QuantumOpticsCert
plain-language theorem explainer
QuantumOpticsCert packages three properties that certify the five-state taxonomy of quantum optics inside Recognition Science: exactly five states exist, the coherent state sits at J-cost zero, and every nonclassical state carries strictly positive J-cost. A researcher deriving photon statistics from the recognition lattice would cite it to fix the classical baseline before computing noise or squeezing. The declaration is a bare structure that simply records the three facts supplied by sibling definitions.
Claim. Let $S$ be the finite set of quantum optical states consisting of the Fock, coherent, squeezed, thermal, and entangled configurations. Then the structure asserts that $|S|=5$, that the J-cost of the coherent state equals zero, and that $J(r)>0$ for every real $r>0$ with $r≠1$.
background
The module treats photons as recognition bosons on the electromagnetic lattice. It introduces the inductive type QuantumOpticalState whose five constructors are Fock, coherent, squeezed, thermal, and entangled; this matches the configDim D=5 fixed by the eight-tick octave in the forcing chain. J-cost is the recognition cost function J(r)=(r+r^{-1})/2-1, which vanishes exactly at the equilibrium point r=1 (coherent state) and is positive for all other positive r.
proof idea
The declaration is a structure definition with no proof body. It directly records the three fields five_states, coherent_zero, and nonclassical_pos; each field is later supplied by the sibling definitions quantumOpticalCount, coherent_state, and nonclassical_state inside the same module.
why it matters
QuantumOpticsCert supplies the interface that quantumOpticsCert instantiates, thereby anchoring the B14/B16 claim that quantum optics emerges with exactly five states and a classical J=0 baseline. It sits downstream of the forcing chain (T7 eight-tick octave, T8 D=3) and upstream of any calculation of photon number statistics or nonclassical noise. No open scaffolding remains inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.