bscCapacity
plain-language theorem explainer
Defines the Shannon capacity of a binary symmetric channel with crossover probability p as one minus the binary entropy of p, written in natural logs scaled by log 2. Information theorists and anyone tracing INFO-002 (ledger bandwidth to channel capacity) would cite it as the BSC special case. The body is a direct closed-form expression, not a derived theorem.
Claim. For crossover probability $p$ with $0 < p < 1$, the binary symmetric channel capacity is $C_{\mathrm{BSC}}(p) = 1 + \frac{p \log p + (1-p)\log(1-p)}{\log 2}$, equivalently $1 - H_2(p)$ where $H_2$ is binary entropy in bits.
background
Module INFO-002 aims to derive Shannon channel capacity from Recognition Science ledger bandwidth: the maximum reliable transmission rate $C = \max_{p(x)} I(X;Y)$ bits per use, with the Gaussian case $C = \tfrac12 \log_2(1+S/N)$ as the textbook target. A discrete memoryless channel is a finite input/output alphabet with a row-stochastic transition kernel.
The binary symmetric channel is the two-symbol special case that flips each bit independently with probability $p$. Its capacity collapses to a one-parameter formula once mutual information is maximized over the input distribution: at the uniform input one obtains $C = 1 - H_2(p)$. Binary entropy $H_2(p) = -p\log_2 p - (1-p)\log_2(1-p)$ is written here via change of base $\log_2 x = \log x / \log 2$.
Sibling definitions in the module supply the general channel structure, input distributions, mutual information, and the abstract capacity as a supremum; this declaration specializes that story to the BSC.
proof idea
Pure definition, not a proof. The right-hand side is the algebraic expansion of $1 - H_2(p)$: binary entropy in nats is $-(p\log p + (1-p)\log(1-p))$, division by $\log 2$ converts to bits, and the leading $1$ is the noiseless binary capacity (one bit per use). The hypothesis $0 < p < 1$ keeps the logs defined and finite. No lemmas are applied.
why it matters
Supplies the standard BSC capacity formula inside the INFO-002 program that wants channel capacity to emerge from ledger recording bandwidth rather than as an external Shannon postulate. It sits beside channelCapacity, mutual-information bounds, and capacity_from_ledger as the concrete two-symbol benchmark against which ledger-derived rates can be checked.
No downstream consumers are wired yet (used_by is empty), so the declaration is presently a named constant in the information layer rather than a forcing-chain step. It does not itself invoke T5–T8, the Recognition Composition Law, or phi-ladder mass formulae; its role is classical information theory scaffolding that the RS ledger story is meant to recover.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.