coherent_poissonian
plain-language theorem explainer
The declaration establishes that the J-cost vanishes at unit argument, identifying coherent light with Poissonian photon statistics in the Recognition Science cost model. Quantum optics researchers would cite this when mapping the five photon regimes to J-cost values. The proof is a direct one-line application of the base unit lemma for J-cost.
Claim. $J(1) = 0$, where $J$ is the J-cost function, which characterizes coherent light exhibiting Poissonian photon statistics.
background
The Photon Statistics from RS module identifies photon number statistics with the J-cost distribution. It enumerates five canonical regimes (super-Poissonian, Poissonian, sub-Poissonian, Fano, Mandel Q) corresponding to configDim D = 5. Coherent light is assigned J = 0 and thus Poissonian statistics, while thermal light has J > 0 and super-Poissonian statistics. The upstream lemma Jcost_unit0 states that J(x) = (x-1)^2 / (2x) and evaluates to zero at x = 1.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_unit0 from the Cost module.
why it matters
This supplies the coherent_zero field inside the photonStatCert definition that certifies the five photon statistics regimes. It anchors the Poissonian case for coherent light within the Recognition Science framework and connects to the J-uniqueness step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.