Physics Quantum Optics From Rs

Quantum states of light

Quantum optics is the physics of light at its most fundamental level, where light behaves not as a continuous wave but as discrete particles called photons. The standard theory recognizes five canonical states that a quantum optical system can occupy: Fock states (fixed photon number), coherent states (the closest quantum analog to classical light), squeezed states (reduced noise in one quadrature), thermal states (blackbody radiation), and entangled states (non-classical correlations). These five states form the basic vocabulary of quantum optics laboratories worldwide.

The theory's history runs from Planck's 1900 quantization of energy through Glauber's 1963 formalization of coherent states, which won the Nobel Prize in 2005. Coherent states are special because they minimize the Heisenberg uncertainty product while maintaining a well-defined phase, making them the standard description of laser light. Fock states with n > 0 photons carry quantum noise above this classical baseline, while squeezed states redistribute that noise between conjugate variables.

In Recognition Science, the framework models each of these five states as a distinct configuration on a recognition lattice, a discrete record of events. The framework's central cost function J(x) = (x + 1/x)/2 - 1 assigns a numerical cost to each state. The coherent state receives cost J(1) = 0, marking it as the classical equilibrium. Every other state with r ≠ 1 receives positive cost J(r) > 0, quantifying the quantum noise above the classical baseline. This gives a clean numerical ordering: classical light costs nothing, quantum light costs something.

The machine-checked library of formal theorems proves these claims directly. The theorem quantumOpticalCount establishes that exactly five states exist in this classification. The theorem coherent_state proves J(1) = 0, and nonclassical_state proves that any state with r ≠ 1 has positive cost. Together they form a certificate, a packaged proof object, that the five-state classification and the cost separation are consistent with the framework's axioms.

What this establishes in plain terms is a bridge: the abstract cost function derived from recognition principles reproduces the standard five-state taxonomy of quantum optics, and it assigns the coherent state its familiar role as the classical limit. The framework does not add new physics here; it shows that the existing structure of quantum optics fits naturally into the recognition cost picture, with the coherent state as the unique zero-cost configuration.

theorem quantumOpticalCount : Fintype.card QuantumOpticalState = 5 := by decide

/-- Coherent state: J = 0 (classical light limit). -/
theorem coherent_state : Jcost 1 = 0 := Jcost_unit0

/-- Nonclassical state: J > 0. -/
theorem nonclassical_state {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
    0 < Jcost r := Jcost_pos_of_ne_one r hr hne

What this page does not claim

The framework derives the full dynamical equations of quantum optics; it only classifies states and assigns costs. The coherent state being cost-zero does not imply classical light has no quantum fluctuations; it is the minimum-cost state within the framework. The five-state list is a definitional choice within the framework, not a theorem about all possible quantum states.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Physics/QuantumOpticsFromRS.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: