photonStatCount
plain-language theorem explainer
The theorem asserts that the finite type enumerating photon statistics regimes in Recognition Science has cardinality five. Researchers deriving quantum optics distributions from the J-cost function would cite this result to anchor the five-regime taxonomy. The proof is a direct decision procedure on the inductive type that automatically derives a Fintype instance.
Claim. The set of photon statistics regimes has cardinality five: $|$ {super-Poissonian, Poissonian, sub-Poissonian, Fano, Mandel $Q$} $| = 5$.
background
Photon statistics in Recognition Science are identified with the distribution of J-cost values. The module states that five canonical regimes (super-Poissonian for thermal light with J > 0, Poissonian for coherent light with J = 0, sub-Poissonian for squeezed light, plus Fano and Mandel Q) arise because configDim D = 5. The upstream inductive definition PhotonStatisticsRegime enumerates exactly these five constructors and derives DecidableEq, Repr, BEq, and Fintype.
proof idea
The proof is a one-line term that applies the decide tactic to the Fintype.card expression. The tactic succeeds because the inductive type PhotonStatisticsRegime supplies a canonical Fintype instance via its five constructors.
why it matters
This cardinality supplies the five_regimes field of the PhotonStatCert certificate that closes the photon statistics module. It instantiates the claim that photon number statistics equal the J-cost distribution and aligns with the Recognition Composition Law and the five-dimensional configuration space. The module records zero sorry or axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.