channelCapacity
plain-language theorem explainer
Channel capacity is the supremum of mutual information I(X;Y) over all input distributions on a discrete memoryless channel. Anyone deriving Shannon rates from Recognition ledger bandwidth, or proving non-negativity and coding bounds in this module, cites this definition. It is a noncomputable real-valued supremum, not a proved existence claim.
Claim. For a discrete memoryless channel with finite input alphabet size $n$, output alphabet size $m$, and transition kernel $P(y\mid x)$, the channel capacity is $C = \sup_p I(X;Y)$, where the supremum runs over all probability distributions $p$ on the input alphabet and $I(X;Y)$ is the mutual information induced by $p$ and the kernel.
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. Classically, $C = \max_{p(x)} I(X;Y)$ bits per use is the maximum reliable transmission rate; for a Gaussian channel the closed form is $\tfrac12\log_2(1+S/N)$.
A channel here is a discrete memoryless structure: finite input and output alphabet sizes, a transition map $P(y\mid x)$ that is nonnegative and row-stochastic. An input distribution is a probability vector on the input alphabet. Mutual information is the usual $I(X;Y)$ built from the joint induced by $p$ and the kernel (siblings also record nonnegativity and symmetry of that quantity).
Upstream cost and entropy objects in the monolith (shifted cost $H = J+1$, configuration defect entropy, horizon microstate entropy) supply the broader RS information language; this definition stays at the classical Shannon layer and packages capacity as a supremum ready for ledger comparison.
proof idea
Pure definition, not a proof. The body is the Lean supremum ⨆ over the type of input distributions of the already-defined mutual information functional. No tactics, no lemmas, no existence or attainment argument: capacity is named as that real number (possibly $±∞$ in principle, later controlled by sibling bounds).
why it matters
This is the central named quantity of INFO-002. Downstream, capacity_nonneg unfolds it and shows $C \ge 0$ because mutual information is nonnegative for every input distribution and the family is bounded above (by $\log(nm)$), so the supremum of a nonnegative bounded-above family is nonnegative.
Sibling results (mutual_info_bounded, shannons_theorem, capacity_from_ledger) sit on top of the same package: classical coding bounds and the RS claim that capacity emerges from ledger bandwidth rather than being postulated. In the wider framework it is the information-theoretic rate object against which eight-tick register and defect-entropy bookkeeping can be compared; it does not itself invoke T5–T8 or the RCL, but it is the Shannon endpoint those ledger arguments are meant to recover.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.