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