quantumOpticsCert
plain-language theorem explainer
The definition supplies a concrete record witnessing that exactly five quantum optical states exist under the Recognition Science J-cost, with the coherent state at J-cost zero and all nonclassical states having positive J-cost. A physicist deriving quantum optics from the recognition lattice would cite this to anchor the state count and equilibrium properties. It is assembled by direct record construction from the cardinality theorem and the two J-cost lemmas.
Claim. Define the quantum optics certificate as the structure whose fields assert that the cardinality of the set of quantum optical states equals 5, that the J-cost of the unit element is zero, and that the J-cost is strictly positive for every positive real number different from one.
background
The module treats photons as recognition bosons on the EM lattice. Five canonical states (Fock, coherent, squeezed, thermal, entangled) arise because the configuration dimension equals 5. The J-cost function measures deviation from recognition equilibrium: coherent states sit at J-cost zero while nonclassical states lie above it. Upstream, quantumOpticalCount proves the cardinality equals 5 by direct enumeration, coherent_state proves Jcost(1) = 0 via the unit property of Jcost, and nonclassical_state proves positivity of Jcost(r) for r > 0, r ≠ 1.
proof idea
One-line record constructor that assigns the five_states field to the quantumOpticalCount theorem, the coherent_zero field to the coherent_state theorem, and the nonclassical_pos field to the nonclassical_state theorem.
why it matters
This definition closes the QuantumOpticsFromRS module by exhibiting an explicit certificate that the five-state taxonomy and J-cost separation hold inside Recognition Science. It supplies the concrete witness required by any downstream derivation that treats quantum optics as a recognition phenomenon on the lattice. The construction uses only zero-sorry lemmas and thereby confirms the module claim of no axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.