correction_RS_one_band
plain-language theorem explainer
The theorem shows the Recognition Science correction to Shannon capacity at message length 1 lies strictly between 0 and 1. Information theorists deriving finite-N channel bounds from the J-cost framework cite this to confirm the deviation occupies less than one bit. The proof rewrites the term at N=1 then applies positivity and comparison rules for the base-2 logarithm together with the ordering properties of phi.
Claim. $0 < C(1) < 1$ where $C(N) = C_0(N) - C_{RS}(N)$ denotes the Recognition Science correction term, $C_0(N) = N$ is the classical capacity in bits, and $C_{RS}(N) = N - 1$ is the finite-N RS capacity with the explicit form $C(1) = 1$ at unit length.
background
The module derives the finite-N correction to classical Shannon capacity from the J-cost on message ensembles in Recognition Science. The RS capacity takes the form $C_{RS}(N) = 1 - 1$ so the correction equals $1$ and the module records the bandedness claim $0 < 1 < 1$ at $N=1$. Upstream lemmas supply the positivity of phi and the strict inequality $1 < phi$ used to bound the argument of the logarithm.
proof idea
The tactic proof rewrites via the at-one evaluation lemma, introduces positivity of phi, shows the argument exceeds 1 and applies the logb positivity rule. For the upper bound it invokes the one-less-than-phi lemma to obtain $1/phi < 1$, deduces the argument is less than 2, compares the logb value to 1 via the logb comparison lemma, and closes with linarith.
why it matters
The result supplies the correction_at_one_band field inside the master certificate shannonAsJCostLimitCert. It completes the algebraic bandedness statement for the unit-length case in the finite-N RS formula, consistent with the phi fixed point and the eight-tick octave structure. The module falsifier remains any finite-N channel whose measured capacity deviates from the RS expression by more than one percent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.