IndisputableMonolith.Information.ChannelCapacity
Defines discrete memoryless channels, input distributions, mutual information, and channel capacity in the Recognition Science information layer. Links classical Shannon capacity to the RS cost/ledger structure via a capacity-from-ledger construction. Physicists citing RS information bounds or eight-tick coding limits would use this module. Mostly definitional scaffolding with nonnegativity, symmetry, and a Shannon-style theorem.
claimA discrete memoryless channel $W$ with input distributions $p$, mutual information $I(X;Y)$, and capacity $C = \sup_p I(X;Y)$. Includes nonnegativity and symmetry of $I$, a uniform distribution, a Shannon-style coding bound, and a map from RS ledger/cost data to a capacity value.
background
Classical discrete memoryless channel (DMC) theory: a channel is a conditional kernel from a finite input alphabet to an output alphabet. An input distribution $p$ induces a joint law; mutual information $I(X;Y)$ measures the reduction in uncertainty about the input given the output. Channel capacity is the supremum of $I$ over input laws.
The module sits in the RS Information domain and imports Constants (RS time quantum $\tau_0 = 1$ tick) and Cost (the $J$-cost / recognition cost layer). Sibling objects include Channel, InputDistribution, mutualInformation, channelCapacity, uniformDistribution, and capacity_from_ledger, so the intent is to restate Shannon quantities in Lean and tie them to the ledger cost structure used elsewhere in the monolith.
Local setting is definitional plus elementary inequalities (nonnegativity, symmetry, boundedness) rather than a full asymptotic coding theorem with error exponents.
proof idea
Definition module with supporting lemmas. Core objects (Channel, InputDistribution, mutualInformation, channelCapacity, uniformDistribution) are introduced as defs. Elementary properties (mutual_information_nonneg, mutual_information_symmetric, mutual_info_bounded, capacity_nonneg, uniform_sum_one) are short inequality or normalization arguments. shannons_theorem packages a Shannon-style capacity statement; capacity_from_ledger bridges RS cost/ledger data into a capacity value. No deep analytic machinery; structure is defs plus elementary real/probability facts from Mathlib.
why it matters in Recognition Science
Gives the Information domain a standard channel-capacity vocabulary so later RS results can quote $C$ and $I(X;Y)$ without leaving the monolith. The distinctive RS hook is capacity_from_ledger, which routes capacity through the cost layer imported from Cost, consistent with recognition cost $J$ and the forcing chain's information-theoretic side (eight-tick octave, discrete ticks via $\tau_0$).
No downstream used_by edges are recorded yet, so this module is presently a leaf provider: it supplies types and lemmas for future coding, ledger, or alpha-band information bounds rather than closing a named parent theorem. It does not itself force $D=3$ or $\phi$; it only stages classical capacity language inside RS units.
scope and limits
- Does not prove a full asymptotic noisy-channel coding theorem with error exponents or random coding bounds.
- Does not derive capacity numerical values for concrete RS physical channels.
- Does not force phi, eight-tick structure, or D=3 from capacity axioms alone.
- Does not treat continuous-alphabet or quantum channels.
- Does not yet show recorded downstream theorems that consume these defs.
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