gaussian_capacity_increases_with_snr
plain-language theorem explainer
Gaussian channel capacity is strictly monotone in signal power at fixed noise: larger SNR yields strictly larger capacity. Anyone comparing SNR regimes in the RS information layer (ledger bandwidth, Shannon rate) would cite this. The proof unfolds the closed form (1/2)log₂(1+S/N) and applies positivity plus log monotonicity.
Claim. Let $S_1,S_2,N>0$ be real signal and noise powers with $S_2>S_1$. Then the Gaussian channel capacity satisfies $\tfrac12\log_2(1+S_2/N)>\tfrac12\log_2(1+S_1/N)$.
background
Module INFO-002 derives Shannon channel capacity from RS ledger bandwidth: the maximum reliable rate $C=\max_{p(x)}I(X;Y)$ bits per use. For an additive white Gaussian noise channel the maximizer is known in closed form, $C=\tfrac12\log_2(1+S/N)$ bits per symbol, where $S$ is signal power and $N$ is noise power (SNR $=S/N$).
In Recognition Science that formula is read as a ledger bandwidth bound: the fundamental tick $\tau_0=1$ and the eight-tick octave fix the discrete recording rate against which continuous Gaussian rates are compared. The present lemma is the elementary SNR-monotonicity fact for that closed form, needed before any comparison of ledger-limited rates across power levels.
proof idea
Unfold the definition of Gaussian capacity to $\mathrm{log}(1+S/N)/(2,\mathrm{log},2)$. From $S_2>S_1$ and $N>0$ obtain $S_2/N>S_1/N$ by right-division, then $1+S_2/N>1+S_1/N$ by linarith. Positivity gives $1+S_1/N>0$, so Real.log is strictly increasing on that ray and yields a strict log inequality. The denominator $2,\mathrm{log},2$ is positive (log 2 > 0), so dividing preserves the strict inequality.
why it matters
Fills the elementary comparison step inside INFO-002 (channel capacity from ledger bandwidth). Without SNR monotonicity one cannot argue that raising ledger signal power strictly raises the Shannon rate bound, nor compare Gaussian rates to the discrete eight-tick recording ceiling. Downstream quantum-capacity remarks in the same module (classical $C$, quantum $Q$, entanglement-assisted $C_E$) inherit the same SNR ordering once reduced to Gaussian noise models. No parent theorem currently depends on it in the graph; it is infrastructure for later capacity comparisons rather than a forcing-chain landmark (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.