ProbDist
plain-language theorem explainer
ProbDist defines a discrete probability distribution over n outcomes as a map from Fin n to reals that is nonnegative and sums to one. Information theorists in the Recognition Science setting cite this structure when showing Shannon entropy equals expected J-cost over distributions. The declaration is a direct structure with three field conditions that encode the probability axioms.
Claim. A discrete probability distribution over $n$ outcomes is a function $p : [n] → ℝ$ such that $p_i ≥ 0$ for all $i$ and $∑_{i=1}^n p_i = 1$.
background
Recognition Science derives Shannon entropy from the J-cost J(x) = ½(x + x^{-1}) - 1 applied to probability ratios. Module INFO-001 shows entropy as the expected J-cost over distributions, with uniform maximizing entropy and deterministic cases yielding zero cost. ProbDist n supplies the type of discrete distributions on n points; its nonneg and normalized fields enforce the axioms. An upstream sibling uniform constructs the equal-probability case via positivity and sum lemmas. A related structure in VariationalFreeEnergyFromRCL uses strict positivity instead.
proof idea
This is a structure definition. The three fields directly record the probability vector, the nonnegativity condition, and the normalization sum. No lemmas or tactics are invoked; the declaration serves as the foundational type for entropy and J-cost calculations downstream.
why it matters
ProbDist anchors the INFO-001 derivation of Shannon entropy from J-cost in the Recognition framework. It feeds theorems establishing nonnegativity of entropy, zero entropy for deterministic distributions, and equality between Shannon entropy and total J-cost. These results connect information measures to the J-uniqueness and self-similar fixed point from the forcing chain. The structure is referenced in 25 downstream declarations, including entropy_is_expected_surprisal and shannon_equals_jcost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.