gaussianCapacity
plain-language theorem explainer
Classical AWGN capacity as a real function of signal power S and noise power N: C = (1/2) log₂(1 + S/N) bits per symbol. Cited by anyone comparing ledger-derived bandwidth to the Shannon Gaussian benchmark in INFO-002. The body is a direct closed-form definition (change-of-base log), not a derived theorem.
Claim. For signal power $S > 0$ and noise power $N > 0$, the Gaussian channel capacity is $C(S,N) = \frac{1}{2}\log_2\bigl(1 + S/N\bigr)$ bits per symbol.
background
Module INFO-002 targets Shannon channel capacity from Recognition Science ledger structure. Capacity is the maximum reliable rate $C = \max_{p(x)} I(X;Y)$ bits per use. For the real additive white Gaussian noise channel the closed form is the half-log SNR formula quoted in the module doc.
Here $S$ and $N$ are signal and noise powers (strictly positive so the ratio and logs sit in the intended regime). Mathlib log is converted to base 2 by dividing by $\log 2$, and the factor $1/2$ is the standard real-symbol (one degree of freedom) normalization. Sibling material in the module includes mutual information, its nonnegativity and symmetry, capacity as a supremum over input distributions, and a ledger-bandwidth construction of capacity.
proof idea
Definition only: the value is written as $\log(1+S/N)/(2\log 2)$. No lemmas, no tactics. Positivity hypotheses on $S$ and $N$ keep the quotient and logarithms in the classical AWGN domain.
why it matters
Supplies the classical Gaussian benchmark inside the INFO-002 program (channel capacity from ledger bandwidth). Immediate consumer is the monotonicity result that this capacity strictly increases with SNR at fixed noise. The module frames capacity as the fundamental rate at which the ledger can record and transmit information; this definition is the AWGN yardstick against which ledger-derived capacity is checked. It is not a T0–T8 forcing step, nor a derivation from the Recognition Composition Law; it is the information-theoretic reference formula the ledger story must eventually match or explain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.