photonStatCount
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.
claimThe 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 in Recognition Science
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.
scope and limits
- Does not assign explicit J-cost values to each regime.
- Does not derive the regimes from the Recognition Composition Law.
- Does not prove the physical light-type correspondences beyond module documentation.
- Does not supply experimental falsification criteria.
Lean usage
def photonStatCert : PhotonStatCert where five_regimes := photonStatCount coherent_zero := coherent_poissonianformal statement (Lean)
29theorem photonStatCount : Fintype.card PhotonStatisticsRegime = 5 := by decide
proof body
Term-mode proof.
30
31/-- Coherent light (Poissonian): J = 0. -/