photonStatCert
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.