IndisputableMonolith.Information.ChannelCapacity
Formalizes discrete memoryless channels, mutual information, and Shannon capacity inside the Recognition Science information layer. Defines capacity as the supremum of mutual information over input distributions, records nonnegativity, symmetry, and elementary bounds, and exposes a ledger-to-capacity bridge. Information theorists working in RS units would cite it for capacity statements. The module is mostly definitions plus short inequality proofs from Mathlib.
claimA discrete memoryless channel $W$, input distributions $p$ on a finite alphabet, mutual information $I(X;Y)$, and channel capacity $C(W)=\sup_p I(X;Y)$. Supporting facts: $I\ge 0$, symmetry in the usual sense, a uniform input distribution, and a map from ledger data to a capacity value, together with a Shannon coding bound sketch.
background
Classical discrete memoryless channel (DMC) theory: a channel is a conditional kernel from a finite input alphabet to a finite output alphabet. An input distribution $p$ induces a joint law on $(X,Y)$; mutual information $I(X;Y)$ measures the reduction in uncertainty about $Y$ given $X$ (equivalently the KL gap from the product of the margins). Capacity is the best rate achievable by coding, realized as $\sup_p I(X;Y)$.
The module sits in the RS Information domain and imports Constants (RS time quantum $\tau_0=1$ tick) and Cost (the $J$-cost calculus). Sibling objects include Channel, InputDistribution, mutualInformation, channelCapacity, uniform input, nonnegativity and symmetry of $I$, a mutual-info bound, Shannon's theorem stub, and capacity_from_ledger.
Local setting: discrete, finite alphabets; no continuous channels or multiuser networks. The ledger bridge is the RS-specific hook that ties abstract capacity back to recognition bookkeeping.
proof idea
Definition-first module. Channel, input distribution, mutual information, and capacity are introduced as data and real-valued functionals. Nonnegativity and symmetry of mutual information are short inequality arguments (KL or entropy identities via Mathlib). Uniform distribution is the normalized counting measure on a finite set; its mass sums to one by a direct sum. Capacity nonnegativity follows from $I\ge 0$. Shannon's theorem and capacity-from-ledger are thin wrappers or interfaces that package the classical coding bound and the RS ledger map; they are not deep analytic developments inside this file.
why it matters in Recognition Science
Gives the Information domain a standard Shannon capacity object so later RS arguments can quote $C(W)$ and $I(X;Y)$ without leaving the monolith. The ledger bridge (capacity_from_ledger) is the distinctive RS landing: it connects recognition bookkeeping to an information-theoretic rate. Downstream use list is currently empty, so the module is foundational rather than a leaf lemma. It does not itself force $\phi$, the eight-tick octave, or $D=3$; those live in the UnifiedForcingChain. Anyone proving rate limits, coding bounds, or ledger-derived capacities in RS units would import this file.
scope and limits
- Does not treat continuous-alphabet or Gaussian channels.
- Does not prove strong converse or error-exponent refinements.
- Does not derive capacity from the J-cost functional equation alone.
- Does not force phi, eight-tick structure, or spatial dimension D=3.
- Does not supply multiuser, network, or quantum channel capacity.
depends on (2)
declarations in this module (20)
-
structure
Channel -
structure
InputDistribution -
def
mutualInformation -
theorem
mutual_information_nonneg -
theorem
mutual_information_symmetric -
def
channelCapacity -
theorem
mutual_info_bounded -
theorem
uniform_sum_one -
def
uniformDistribution -
theorem
capacity_nonneg -
theorem
shannons_theorem -
theorem
capacity_from_ledger -
def
fundamentalBitRate -
def
bscCapacity -
def
gaussianCapacity -
theorem
gaussian_capacity_increases_with_snr -
def
quantumCapacities -
theorem
holevo_bound -
def
applications -
structure
ChannelCapacityFalsifier