ProbabilityDistribution
plain-language theorem explainer
ProbabilityDistribution encodes a discrete probability measure on a finite set Ω with non-negative components that sum to one. Researchers working on Recognition Thermodynamics cite it when stating the H-theorem, free-energy monotonicity under coarse-graining, or the arrow of time. The declaration is a direct structure definition that imposes the two axioms with no proof obligations.
Claim. A probability distribution on a finite set $Ω$ is a function $p:Ω→ℝ$ such that $p(ω)≥0$ for all $ω∈Ω$ and $∑_{ω∈Ω}p(ω)=1$.
background
The Recognition Thermodynamics module extends the T=0 J-cost minimization of the forcing chain to finite Recognition Temperature TR. Probability distributions supply the state descriptors for the Gibbs measure $p(x)∝exp(-J(x)/TR)$ and for the recognition entropy $S_R(p)=-∑p(ω)ln(p(ω))$. The module imports the Energy abbrev from RSNativeUnits and the Born-rule probability from QuantumLedger, where the latter is defined as Complex.normSq of the amplitudes.
proof idea
The declaration is a structure definition that directly packages the function p together with the non-negativity and normalization fields. No lemmas or tactics are invoked; the two fields simply record the mathematical requirements for a probability measure on a Fintype.
why it matters
This structure is the common type appearing in the H-theorem for Recognition, the coarse-graining monotonicity theorem, the rs-arrow-of-time definition, and the entropy-maximizer-is-Gibbs result. It supplies the state space on which the variational identity $F_R(p)=F_R(Gibbs)+TR·D_KL(p||Gibbs)$ is stated, thereby connecting the phi-ladder discretization of the foundation to finite-temperature dynamics. It touches the open question of how the eight-tick cycle furnishes the fundamental time unit for relaxation trajectories.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.