uniform
plain-language theorem explainer
The uniform distribution on n positive outcomes sets each probability to exactly 1/n. Information theorists working from the J-cost structure cite it as the maximum-entropy reference measure when deriving Shannon entropy via the Recognition Composition Law. The definition is a direct structure literal that populates the probability field with a constant function and discharges the two axioms by the positivity tactic and a finite-sum simplification.
Claim. Let $n$ be a positive natural number. The uniform distribution $u$ on $n$ outcomes is the map $u(i) = 1/n$ for each $i$ in the finite set of size $n$, with the properties that $u(i) > 0$ for all $i$ and that the sum of all $u(i)$ equals 1.
background
ProbDist n is the structure whose fields are a function probs from the finite set of size n into the reals, together with proofs that every value is non-negative and that the sum over the whole set equals one. The module Information.ShannonEntropy uses this structure to express Shannon entropy as the expected J-cost of a probability distribution, where J is the Recognition Science cost function. Upstream, the entropy of any configuration is defined to be its total defect, and the shifted cost H(x) = J(x) + 1 satisfies the d'Alembert form of the Recognition Composition Law.
proof idea
The definition is a direct structure literal. It sets the probability field to the constant function returning 1/n, proves non-negativity by the positivity tactic, and proves normalization by rewriting the sum of a constant over a finite set of cardinality n and clearing the resulting denominator.
why it matters
This definition supplies the reference measure needed for the maximum-entropy theorem and the equality between Shannon entropy and total J-cost that appear later in the same module. It therefore anchors the derivation of information measures from the J-cost functional described in the module documentation. The construction is invoked whenever a uniform bound or maximum-entropy state is required in the surrounding information-theoretic arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.