mutual_information_nonneg
plain-language theorem explainer
Mutual information of a discrete memoryless channel under any input law is non-negative. Anyone proving channel capacity bounds or ledger-bandwidth rates in the INFO-002 development cites this positivity fact. The argument is a one-line consequence of the definition as a max with zero.
Claim. For every discrete memoryless channel and every probability distribution on its input alphabet, the mutual information satisfies $I(X;Y)\ge 0$.
background
The module targets Shannon channel capacity as a ledger-bandwidth rate: $C=\max_{p(x)} I(X;Y)$ bits per use, with the RS claim that this maximum is forced by how fast the ledger can record transitions.
A channel here is a discrete memoryless channel: finite input and output alphabets together with a row-stochastic transition kernel $P(y|x)\ge 0$. An input distribution is a non-negative vector on the input alphabet summing to one.
Mutual information is introduced in the KL form $I(X;Y)=D_{\mathrm{KL}}(P_{XY}|P_X\otimes P_Y)$, which is classically non-negative. In this file it is defined, for simplicity, as $\max(0,\sum_{x,y}\cdots)$, so non-negativity is built into the carrier rather than derived from entropy identities.
proof idea
Unfold the definition of mutual information. That definition is literally $\max(0,S)$ for a real sum $S$ over input-output pairs. The inequality $\max(0,S)\ge 0$ is then le_max_left 0 _. No entropy calculus or channel axioms are used beyond the type of the arguments.
why it matters
This is the base positivity lemma for the INFO-002 stack (channel capacity from ledger bandwidth). Downstream, capacity_nonneg quotes it directly: capacity is a supremum of mutual informations, hence non-negative once every summand is. That feeds the larger claim that the ledger's reliable transmission rate is a well-defined non-negative real, before any comparison to the classical Gaussian formula $\tfrac12\log_2(1+S/N)$ or to RS constants. It does not yet touch the forcing chain (T5–T8) or the mass ladder; it only secures the information-theoretic lower bound side of the capacity story.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.