PhotonStatCert
PhotonStatCert defines a structure certifying exactly five photon statistics regimes in the J-cost distribution together with the identity Jcost(1) = 0. Quantum-optics researchers working inside the Recognition Science derivation of light statistics would cite this certificate to fix the classification of super-Poissonian through Mandel-Q regimes. The definition is a direct structure whose two fields are supplied by the Fintype cardinality of the inductive regime type and the algebraic zero of J at unity.
claimA structure certifying that the set of photon statistics regimes has cardinality 5 and that the J-cost function satisfies $J(1)=0$.
background
The module treats photon number statistics as the distribution of J-cost values. PhotonStatisticsRegime is the inductive enumeration with five constructors (superPoissonian, poissonian, subPoissonian, fano, mandelQ) that derives DecidableEq, Repr, BEq and Fintype. This enumeration realises the statement that configDim D equals 5. The J-cost is the Recognition Science function $J(x)=(x+x^{-1})/2-1$, which vanishes at $x=1$ and thereby characterises coherent states.
proof idea
The declaration is a structure definition. Its first field is discharged by the Fintype instance on PhotonStatisticsRegime. Its second field is discharged by the lemma coherent_poissonian that establishes Jcost(1)=0. The downstream definition photonStatCert simply assembles these two facts into an instance of the structure.
why it matters in Recognition Science
PhotonStatCert supplies the type for the theorem photonStatCert that constructs the concrete certificate. It realises the B14/B16 claim that photon statistics comprise five regimes whose count matches configDim D=5, and that coherent light corresponds to the zero of J. The certificate therefore anchors the RS classification of quantum versus classical light inside the eight-tick octave and the phi-ladder.
scope and limits
- Does not derive the J-cost distribution from the forcing chain.
- Does not assign numerical values to the five regimes.
- Does not prove the physical mapping of each regime to observed light.
- Does not extend the classification beyond the five enumerated regimes.
formal statement (Lean)
34structure PhotonStatCert where
35 five_regimes : Fintype.card PhotonStatisticsRegime = 5
36 coherent_zero : Jcost 1 = 0
37