Channel
plain-language theorem explainer
Defines a discrete memoryless channel: finite input and output alphabets with a row-stochastic transition kernel P(y|x). Anyone building mutual information, Shannon capacity, or RS ledger-bandwidth bounds cites this carrier type. It is a pure structure with nonnegativity, normalization, and nonempty-alphabet fields; no proof body.
Claim. A discrete memoryless channel consists of positive integers $n$ (input alphabet size) and $m$ (output alphabet size) together with a kernel $P:\{0,\ldots,n-1\}\times\{0,\ldots,m-1\}\to\mathbb{R}$ such that $P(y\mid x)\ge 0$ for all $x,y$ and $\sum_y P(y\mid x)=1$ for each fixed $x$.
background
Module INFO-002 aims to derive Shannon channel capacity from Recognition Science ledger bandwidth. Classically, capacity is $C=\max_{p(x)} I(X;Y)$ bits per use; for a Gaussian channel one recovers $\tfrac12\log_2(1+S/N)$. In RS the same quantity is read as the fundamental rate at which the ledger can record and transmit information.
The carrier needed for that program is the standard DMC: finite alphabets and a conditional probability kernel. Sibling definitions in the module (input distributions, mutual information, capacity as a supremum) all take this structure as their first argument. Upstream probability notions (Born-rule configuration probabilities on the quantum ledger, Boltzmann level probabilities) supply the same nonnegativity-plus-normalization pattern that the transition fields enforce here.
proof idea
No proof: this is a structure declaration. The fields package the classical DMC data (sizes, kernel, nonnegativity, row-stochasticity, nonempty alphabets) so downstream theorems can quantify over a single well-typed object rather than a loose tuple of hypotheses.
why it matters
This is the base type for the whole ChannelCapacity development: mutual information, capacity nonnegativity, Shannon's theorem sketch, and capacity-from-ledger all consume Channel. Downstream gravity and QG modules reuse the same channel language for strong-field observables, ringdown echo models (RS prediction $\phi^{-1}$), and amplitude-linear quantum-channel certificates. On the public spine it sits under the information layer that the ledger-bandwidth story must eventually discharge. It does not itself force $\phi$, the eight-tick octave, or $D=3$; those enter only when capacity is specialized to RS-native rates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.