coherent_state
plain-language theorem explainer
The theorem establishes that the J-cost vanishes at the unit argument, identifying the classical coherent state of light in the RS quantum optics model. Researchers certifying canonical quantum optical states on the recognition lattice would cite this equality when constructing the five-state certificate. The proof is a direct one-line application of the unit lemma for the J-cost function.
Claim. $J(1) = 0$, where $J(x) = (x-1)^2 / (2x)$ denotes the J-cost of a recognition element.
background
The J-cost function is defined by the squared ratio $J(x) = (x-1)^2 / (2x)$, which measures deviation from recognition equilibrium. In the Quantum Optics from RS module, light states are modeled as recognition bosons on an EM lattice, with exactly five canonical configurations (Fock, coherent, squeezed, thermal, entangled) corresponding to configDim D = 5. The coherent state is singled out as the equilibrium case where this cost vanishes, while Fock states with n > 0 carry positive cost above the baseline.
proof idea
One-line wrapper that applies the Jcost_unit0 lemma from the Cost module (and its JcostCore sibling). The lemma itself is proved by simp on the definition of Jcost.
why it matters
This equality supplies the coherent_zero field inside the QuantumOpticsCert definition, which packages the five-state count together with the classical and nonclassical markers. It directly instantiates the classical light limit inside the RS framework, where coherent states mark recognition equilibrium on the phi-ladder. The result closes one of the five state slots required by the module's certification of quantum optics from the underlying recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.