correction_RS_nonneg
plain-language theorem explainer
The RS finite-N correction to Shannon capacity is non-negative for every positive real N. Information theorists deriving finite-N channel capacities from the J-cost framework would cite this to confirm the adjusted capacity stays non-negative. The proof unfolds the correction definition, invokes phi positivity from Constants, applies linarith to bound the log argument above 1, and finishes with Real.logb_nonneg.
Claim. For every real number $N > 0$, $0 ≤ log₂(1 + 1/(φ N))$, where φ is the golden ratio.
background
The module recovers classical Shannon capacity C = log₂ N as the high-N limit of J-cost on message ensembles. At finite N the RS model adds the correction term log₂(1 + 1/(φ N)), with φ drawn from the Constants structure. This non-negativity result is one of the algebraic facts needed to certify the finite-N formula C_RS(N) = log₂ N − correction_RS(N).
proof idea
Unfold correction_RS to expose Real.logb 2 (1 + 1/(Constants.phi * N)). Obtain phi_pos from Constants, derive 0 < 1/(phi N) by div_pos and mul_pos, then apply linarith to get 1 ≤ 1 + 1/(phi N). Finish by calling Real.logb_nonneg with base > 1 and argument ≥ 1.
why it matters
The theorem is invoked inside shannonAsJCostLimitCert to assemble the full certificate for the RS finite-N capacity decomposition. It supplies the algebraic non-negativity piece of the ShannonAsJCostLimit track (F7), ensuring the 1/φ correction vanishes as N → ∞ and remains consistent with the high-N recovery of classical Shannon capacity. The empirical match for actual channels stays a separate hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.