photonStatCert
PhotonStatCert is instantiated as the record asserting exactly five photon statistics regimes together with vanishing J-cost for the coherent unit state. Quantum optics researchers working from Recognition Science would cite the certificate when classifying observed photon counting distributions by J-cost sign and magnitude. The definition is a direct structure constructor that supplies the finite cardinality theorem to the regimes field and the unit J-cost identity to the coherent field.
claimThe photon statistics certificate asserts that the finite type of photon statistics regimes has cardinality five, $|PhotonStatisticsRegime|=5$, and that the J-cost of the unit element vanishes: $J_{cost}(1)=0$.
background
Recognition Science expresses photon number statistics as the distribution induced by the J-cost functional on states. The module identifies five canonical regimes (super-Poissonian, Poissonian, sub-Poissonian, Fano, Mandel Q) whose count equals the configuration dimension D=5. Coherent light corresponds to J-cost zero and therefore Poissonian counting statistics, while thermal and squeezed states carry positive J-cost in the appropriate quadrature.
proof idea
The definition is a one-line record constructor. It assigns the theorem photonStatCount, which proves the cardinality of PhotonStatisticsRegime equals five by decision, to the five_regimes field, and assigns the theorem coherent_poissonian, which reduces Jcost 1 to zero via Jcost_unit0, to the coherent_zero field.
why it matters in Recognition Science
This definition supplies the concrete PhotonStatCert required by the photon statistics module. It closes the local claim that photon statistics are governed by the J-cost distribution with exactly five regimes and coherent states at J=0, thereby linking the Recognition Composition Law to observable quantum optics signatures. No downstream uses appear in the current dependency graph.
scope and limits
- Does not derive explicit probability distributions for each regime.
- Does not prove the sign of J-cost maps to super- versus sub-Poissonian statistics.
- Does not compute Mandel Q or Fano factor expressions from the J-cost functional.
- Does not address experimental tests of the predicted counting statistics.
formal statement (Lean)
38def photonStatCert : PhotonStatCert where
39 five_regimes := photonStatCount
proof body
Definition body.
40 coherent_zero := coherent_poissonian
41
42end IndisputableMonolith.Physics.PhotonStatisticsFromRS