capacity_nonneg
plain-language theorem explainer
Channel capacity of a discrete memoryless channel is always non-negative. Information theorists and RS ledger-bandwidth arguments cite this as the baseline sanity check before coding bounds. The proof realizes capacity as a supremum of mutual informations, exhibits a uniform input whose mutual information is ≥ 0, and bounds the family above by a log of alphabet sizes.
Claim. For every discrete memoryless channel $C$ with finite input and output alphabets, the channel capacity $\mathrm{Cap}(C) := \sup_{p} I(X;Y)$ (supremum of mutual information over input distributions $p$) satisfies $\mathrm{Cap}(C) \ge 0$.
background
Module INFO-002 packages classical Shannon capacity so it can later be identified with Recognition Science ledger bandwidth: the rate at which the ledger records and transmits information. A channel here is a discrete memoryless channel: finite input size, finite output size, and a row-stochastic transition kernel $P(y|x)$ with non-negative entries summing to one in each row.
Mutual information $I(X;Y)$ is the usual non-negative divergence between the joint law and the product of margins. Channel capacity is defined as the supremum of $I(X;Y)$ over input distributions on the finite alphabet. Sibling facts already record that every mutual information is ≥ 0 and that each value is bounded above by $\log(|X|\cdot|Y|)$.
The local goal is not yet the full coding theorem; it is to put the capacity functional on a Lean footing that later results (Shannon coding, capacity-from-ledger) can quote.
proof idea
Unfold capacity to a supremum of mutual informations. Apply the standard comparison that a supremum is at least any particular member once the family is bounded above (le_ciSup_of_le).
Boundedness: take the constant $\log(\mathrm{inputSize}\cdot\mathrm{outputSize})$ and invoke the sibling bound that every mutual information is ≤ that log. Witness value: evaluate mutual information at the uniform input distribution on the nonempty input alphabet; non-negativity of that single value is the sibling mutual_information_nonneg. The supremum is therefore ≥ 0.
why it matters
Elementary non-negativity gate for the INFO-002 program. Capacity is defined as max mutual information; without $C \ge 0$ the subsequent Shannon noisy-channel coding statement and the RS claim that ledger error-correction capacity matches $C$ would be ill-posed. Immediate siblings in the same module are the Shannon theorem stub and capacity_from_ledger.
No recorded downstream dependents yet. Framework placement is the information layer that will connect capacity to ledger bandwidth, not the T0–T8 forcing chain (J-uniqueness, $\varphi$, eight-tick, $D=3$). The module doc frames the end target as deriving Shannon capacity from ledger structure; this lemma only clears the sign of $C$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.