PhotonStatisticsRegime
PhotonStatisticsRegime enumerates the five canonical photon number statistics regimes obtained from J-cost distributions in Recognition Science. Researchers mapping quantum optics to the RS framework cite this inductive type when certifying that exactly five regimes arise for configuration dimension D=5. The definition is a direct enumeration that derives Fintype, enabling immediate cardinality verification in the companion certificate.
claimAn inductive type whose constructors are the five photon statistics regimes: super-Poissonian, Poissonian, sub-Poissonian, Fano factor, and Mandel Q parameter.
background
In Recognition Science, photon number statistics are identified with the distribution of J-costs, where the J-cost function is given by J(x) = (x + x^{-1})/2 - 1. The module states that these statistics yield exactly five canonical regimes when the configuration dimension equals 5. Coherent light (J = 0) produces Poissonian statistics, thermal light (J > 0) produces super-Poissonian statistics, and squeezed light produces sub-Poissonian statistics.
proof idea
The declaration is a direct inductive definition that lists the five constructors and derives the instances DecidableEq, Repr, BEq, and Fintype. No lemmas are invoked; the Fintype derivation is used immediately by the downstream cardinality theorem photonStatCount.
why it matters in Recognition Science
This type supplies the five regimes required by the PhotonStatCert structure, which records both Fintype.card PhotonStatisticsRegime = 5 and the coherent-zero condition Jcost 1 = 0. It implements the B14/B16 depth of the photon-statistics mapping, aligning the five regimes with configDim D = 5 and the J-cost interpretation of light statistics. The definition thereby closes the enumeration step that feeds the certificate used by photonStatCount.
scope and limits
- Does not derive the explicit assignment of J-cost intervals to each regime.
- Does not link the regimes to the forcing-chain steps T0-T8.
- Does not compute numerical statistics for concrete light states beyond the J = 0 case.
- Does not extend the enumeration to configuration dimensions other than 5.
formal statement (Lean)
25inductive PhotonStatisticsRegime where
26 | superPoissonian | poissonian | subPoissonian | fano | mandelQ
27 deriving DecidableEq, Repr, BEq, Fintype
28