InputDistribution
plain-language theorem explainer
Defines a finite input alphabet probability law: n nonnegative real weights on Fin n that sum to one. Anyone stating mutual information, channel capacity, or a uniform prior over the channel input cites this carrier type. There is no proof body; it is a plain structure with three fields.
Claim. For $n \in \mathbb{N}$, an input distribution is a map $p : \{0,\ldots,n-1\} \to \mathbb{R}$ such that $p(i) \ge 0$ for every $i$ and $\sum_{i} p(i) = 1$.
background
Module INFO-002 aims to derive Shannon channel capacity from Recognition Science ledger bandwidth. Capacity is $C = \max_{p(x)} I(X;Y)$ bits per use; the maximizer runs over input laws on a finite alphabet.
An input distribution packages exactly that law: a real vector indexed by Fin n, pointwise nonnegative, and normalized to total mass one. Downstream mutual information is built from the product $p(x),P(y|x)$ against the channel transition kernel, so the type must enforce the probability axioms at the structure level.
The module imports Cost and Constants; the shifted cost $H(x)=J(x)+1$ appears elsewhere in the RS stack, but this structure itself is ordinary finite discrete probability, not a cost identity.
proof idea
No proof. The declaration is a structure with three fields: the probability mass function, a pointwise nonnegativity proof obligation, and a Finset-sum normalization obligation equal to one. Inhabitants are built by supplying those three components (as in the uniform distribution helper).
why it matters
This is the domain type for the capacity supremum. channelCapacity is defined as $\sup$ of mutual information over all InputDistribution on the channel input size; mutualInformation, its nonnegativity theorem, and the log-alphabet upper bound all take an InputDistribution argument. The uniform distribution constructor returns this type and feeds capacity comparisons.
In the INFO-002 program, ledger bandwidth is meant to force Shannon's $C=\max_p I(X;Y)$. Without a typed input law, that maximization has no carrier. The structure does not yet encode RS-specific constraints (phi-ladder, eight-tick octave); it is the classical probability interface the ledger story must eventually specialize.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.