pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Physics.PhotonStatisticsFromRS

show as:
view Lean formalization →

The module derives photon statistics regimes in Recognition Science by tying the J-cost to distribution types. Quantum optics researchers cite it when mapping coherent states to Poissonian counts via the forcing chain. It supplies regime definitions and a direct certification that J equals zero for coherent light.

claimCoherent light satisfies $J=0$ and therefore exhibits Poissonian photon statistics.

background

The module imports the Cost framework, where the J-cost is the function $J(x)=(x+x^{-1})/2-1$ that quantifies deviation from self-similarity. It introduces PhotonStatisticsRegime as the classification of light according to the value of J, together with the count function photonStatCount and the certification PhotonStatCert. The setting is the extraction of observable statistics directly from the unified forcing chain T0-T8.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the photon-statistics layer that lets the J-uniqueness result (T5) and the Recognition Composition Law reach optical observables. The module closes the step from abstract cost to measurable count distributions inside the D=3 spatial setting.

scope and limits

depends on (1)

Lean names referenced from this declaration's body.

declarations in this module (5)