mutualInformation
plain-language theorem explainer
Defines mutual information I(X;Y) for a discrete memoryless channel under a fixed input law, as a non-negative real. Anyone building Shannon capacity or ledger-bandwidth bounds in this module cites it. The body is an explicit double sum of a KL-style integrand, clipped below by zero via max.
Claim. Given a discrete memoryless channel with finite input and output alphabets and transition kernel $P(y\mid x)$, and an input distribution $p$ on the input alphabet, set $p(x,y)=p(x)P(y\mid x)$ and $p(y)=\sum_{x'}p(x')P(y\mid x')$. Define $$I(X;Y)=\max\Bigl(0,\sum_{x,y} p(x,y)\bigl(\log p(x,y)-\log p(y)\bigr)\Bigr),$$ with the summand taken as $0$ whenever $p(x,y)\le 0$ or $p(y)\le 0$.
background
Module INFO-002 aims to derive Shannon channel capacity from Recognition Science ledger bandwidth: the fundamental rate at which the ledger can record and transmit information. The classical target is $C=\max_{p(x)}I(X;Y)$ bits per use.
A channel here is a discrete memoryless channel: finite input size, finite output size, and a transition map $P(y\mid x)$ that is nonnegative and row-stochastic. An input distribution is a nonnegative probability vector on the input alphabet (sums to one).
Mutual information is the usual measure of how much the output reveals about the input. The module doc and local comment present the textbook identities $I(X;Y)=H(Y)-H(Y\mid X)$ and the sum $\sum p(x)P(y\mid x)\log(P(y\mid x)/p(y))$, then adopt a KL-style non-negative formulation for the formal definition.
proof idea
Not a proof: a noncomputable definition. Joint mass is $p(x)P(y\mid x)$; marginal $p(y)$ is the obvious sum over inputs. The double sum over the finite input and output alphabets accumulates $p(x,y)(\log p(x,y)-\log p(y))$ when both masses are strictly positive, else zero. The outer $\max(0,\cdot)$ forces the returned real to be nonnegative by construction, matching the KL non-negativity comment in the source.
why it matters
This is the quantitative core of the channel-capacity stack in INFO-002. Downstream, channel capacity is the supremum of this quantity over input distributions; non-negativity is immediate from the outer max; an upper bound by $\log$ of the product of alphabet sizes is proved by unfolding the same sum.
In the Recognition framing, capacity is meant to emerge from ledger bandwidth rather than as a free Shannon postulate. The definition supplies the classical $I(X;Y)$ object that later results (including the named Shannon theorem and capacity-from-ledger siblings in the module) must match or bound. It does not itself invoke the forcing chain (T5–T8) or the J-cost; those enter only if ledger structure is later identified with the channel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.