correction_RS_tendsto_zero
plain-language theorem explainer
The RS correction term log base 2 of (1 plus 1 over phi N) tends to zero as real N tends to infinity. Information theorists extending Shannon capacity into Recognition Science finite-N models would cite this to recover the classical limit. The proof composes the inner argument limit to one with continuity of the base-2 logarithm at one, then applies logb_one.
Claim. $lim_{N to infty} log_2 (1 + 1/(phi N)) = 0$
background
This module deepens the J-cost formulation of Shannon capacity from ShannonAsJCostLimit. The correction is defined as log base 2 of (1 plus 1 over phi times N), where phi is the self-similar fixed point from the forcing chain. It rests on the prior lemma that the inner argument 1 plus 1 over (phi N) tends to 1 as N to infinity.
proof idea
The tactic proof unfolds the definition of the correction, applies the lemma inner_arg_tendsto_one, establishes continuity of Real.logb 2 at 1 via continuousAt_logb, composes the tendsto maps, and rewrites the target using logb_one to reach the zero neighborhood.
why it matters
This theorem is invoked directly in C_RS_minus_C_classical_tendsto_zero to show the RS-classical gap vanishes, and in shannonHighNLimitCert plus the bundled one-statement theorem that collects positivity, monotonicity, and the limit. It completes the high-N recovery step in the Information track, consistent with the phi-ladder and J-cost composition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.