shannons_theorem
plain-language theorem explainer
Records Shannon's noisy-channel coding theorem as an RS claim: rates below capacity admit arbitrarily reliable coding; rates above force error probability to one. In the ledger picture the same bound is the ledger's error-correction bandwidth. The formal goal is presently ⊤, closed by the trivial term, so the page is a named landmark rather than a proved coding theorem.
Claim. Shannon's noisy-channel coding theorem: if the transmission rate $R$ is strictly less than the channel capacity $C$, there exists a coding scheme with arbitrarily small error probability; if $R > C$, the error probability tends to $1$. In Recognition Science the ledger's error-correction capacity is identified with $C$. (The Lean statement is presently $\top$.)
background
Module INFO-002 aims to derive classical channel capacity from Recognition Science ledger structure. Capacity is the usual mutual-information maximum $C = \max_{p(x)} I(X;Y)$ bits per use (Gaussian form $\tfrac12\log_2(1+S/N)$). The RS claim is that this $C$ is not an external postulate but the ledger's bandwidth: temporal resolution set by the fundamental tick, spatial resolution by voxel size, and energy per bit by the coherence scale $E_{\mathrm{coh}}$.
Upstream ledger structures (double-entry recognition events, quantum-ledger balance as sum of log-ratios) supply the bookkeeping substrate. Sibling definitions in the module introduce channels, input distributions, mutual information, nonnegativity and symmetry of $I(X;Y)$, and channelCapacity as that maximum. The theorem sits immediately before the ledger-bandwidth derivation note that writes $C_{\mathrm{ledger}}$ as (transitions per second) times (bits per transition).
proof idea
Term-mode proof of True by trivial. No lemmas, no unfolding of capacity or mutual information, no coding constructions. The comments above the colon state the classical $R < C$ / $R > C$ dichotomy, but the goal type does not encode those inequalities. Treat as a named placeholder landmark pending a real statement in terms of channelCapacity and error probability.
why it matters
Marks the classical Shannon bound inside the RS information stack so later ledger-bandwidth arguments can cite a single declaration. The module target is to match $C$ to ledger transition rate times bits per transition, tying information limits to the same tick and cost structure used elsewhere in the monolith (recognition events, double-entry balance). No downstream theorems currently depend on it (used_by is empty), so it does not yet feed mass, forcing-chain, or constants results. It does not engage T5–T8, the RCL, or the $\varphi$-ladder; its role is purely informational bookkeeping until a non-trivial statement replaces True.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.