mutual_info_bounded
plain-language theorem explainer
Mutual information I(X;Y) for any discrete memoryless channel and input law is at most log of the product of alphabet sizes. Anyone bounding channel capacity or proving capacity nonnegativity cites this. The proof unfolds the max(0, sum) definition, shows the sum equals a nonpositive conditional-entropy term, and compares both branches to log(nm).
Claim. For every discrete memoryless channel with input alphabet size $n \ge 1$ and output alphabet size $m \ge 1$, and every input distribution $p$ on the input alphabet, the mutual information satisfies $I(X;Y) \le \log(nm)$.
background
Module INFO-002 aims to derive Shannon channel capacity from Recognition Science ledger bandwidth. A channel is a finite input alphabet of size $n$, output alphabet of size $m$, and nonnegative transition kernel $P(y|x)$ that is a probability for each $x$. An input distribution is a nonnegative normalized mass $p$ on the input alphabet.
Mutual information is defined here as $\max\bigl(0,\sum_{x,y} p(x,y)\log(p(x,y)/p(y))\bigr)$, i.e. $\max(0,-H(X|Y))$. The sum is the usual joint-minus-marginal log ratio; the outer max enforces the information-theoretic nonnegativity convention used later for capacity.
The local goal is $C=\max_p I(X;Y)$ as the ledger's reliable transmission rate. An upper bound on $I$ independent of $p$ is the elementary step that makes the supremum well-posed and finite before Shannon-type coding statements.
proof idea
Unfold the mutual-information definition and apply max_le, so both branches must sit under $\log(nm)$.
Left branch: $n,m\ge 1$ (from the channel's nonempty alphabet hypotheses) gives $nm\ge 1$, hence $\log(nm)\ge 0$ by Real.log_nonneg.
Right branch: the double sum is shown $\le 0$ by two nested Finset.sum_nonpos passes. On each $(x,y)$ cell with $p_{xy}>0$ and $p_y>0$, the joint mass is one nonnegative summand of the marginal $p_y$, so $p_{xy}\le p_y$, the ratio is $\le 1$, and $\log(p_{xy}/p_y)\le 0$. Multiplying by $p_{xy}>0$ keeps the term nonpositive; the zero branch is trivial. Transitivity with the already-proved $\log(nm)\ge 0$ finishes.
why it matters
This is the concrete upper bound that lets channel capacity be realized as a real supremum rather than an unbounded search over input laws. Downstream, capacity_nonneg uses exactly this bound as the witness that the set of mutual informations is bounded above, then concludes $C\ge 0$ from nonnegativity of each $I(X;Y)$.
In the INFO-002 program, capacity is the ledger bandwidth: the maximum rate at which the recognition ledger can record and transmit distinctions. The bound is classical information theory, not an RS forcing step (T5–T8), but it is the analytic lid that keeps the RS-native capacity construction finite before linking to eight-tick octave structure and cost algebra elsewhere in the monolith.
Without it, the later Shannon theorem and ledger-capacity bridge in this module have no finite comparison scale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.