uniformDistribution
plain-language theorem explainer
Canonical uniform input law on n symbols (n>0): each coordinate gets probability 1/n. Anyone proving bounds on channel capacity or mutual information cites it as a concrete InputDistribution witness. The body is a structure package: constant probs, positivity for nonnegativity, and the sibling sum-to-one lemma for normalization.
Claim. For every natural number $n>0$, the assignment $i \mapsto 1/n$ on the $n$ input symbols is a valid input distribution: probabilities are nonnegative and sum to $1$.
background
Module INFO-002 aims to recover Shannon channel capacity from Recognition Science ledger bandwidth. Capacity is $C=\max_{p(x)} I(X;Y)$ bits per use; the ledger supplies the fundamental record/transmit rate that plays the role of that bandwidth.
An input distribution on $n$ symbols is a map $\mathrm{Fin},n\to\mathbb{R}$ that is pointwise nonnegative and sums to one over the finite universe. Mutual information $I(X;Y)=H(Y)-H(Y|X)$ is defined on pairs of such laws and a channel kernel; capacity is the supremum of $I$ over input laws.
The uniform law is the simplest normalized nonnegative assignment and is the standard witness when one only needs existence of some input distribution (e.g. to show the capacity supremum is at least zero).
proof idea
Definitional structure construction, not a tactic proof. Probabilities are the constant function $1/n$. Nonnegativity is discharged by the positivity tactic (using $n>0$). Normalization is exactly the sibling lemma that the sum of $n$ copies of $1/n$ equals one. The noncomputable marker is inherited from real division in Mathlib.
why it matters
Supplies the concrete input law used by capacity_nonneg, which states that channel capacity is nonnegative because mutual information is nonnegative for every input distribution and the supremum of a family of nonnegative reals is nonnegative. In the INFO-002 program this is bookkeeping infrastructure: before linking $C$ to ledger bandwidth or stating Shannon's theorem in RS units, one needs a inhabited type of input distributions and easy witnesses. It does not itself encode eight-tick structure, $\varphi$-ladder mass, or the J-cost; those enter only when capacity is tied back to the ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.