correction_RS
plain-language theorem explainer
correction_RS supplies the explicit finite-N correction to the Shannon capacity in the RS framework as the base-2 log of (1 + 1/(phi N)). Researchers in finite-blocklength information theory would cite this term when contrasting classical limits with J-cost predictions. The definition is introduced directly as a closed-form expression using the phi constant from the CPM bundle.
Claim. The RS finite-N correction term is given by $log_2(1 + 1/ (phi N))$, where phi is the golden ratio constant from the CPM constants bundle.
background
In the ShannonAsJCostLimit module the classical channel capacity C = log2 N is recovered as the high-N limit of J-cost on a message ensemble. At finite N the RS model introduces a 1/phi-rational correction to this limit. The module setting is Track F7, where Shannon entropy appears as a J-cost limit with the correction vanishing as N tends to infinity.
proof idea
This is a direct definition that sets the correction to Real.logb 2 (1 + 1 / (Constants.phi * N)). No lemmas are applied; it functions as an immediate abbreviation of the correction expression.
why it matters
The definition is referenced by the master certificate ShannonAsJCostLimitCert and supports the decomposition C_classical(N) - C_RS(N) = correction_RS(N). It supplies the finite-N term in the Shannon-as-J-cost-limit track, consistent with the phi constant forced by J-uniqueness in the unified forcing chain. The module treats empirical validation for finite-N coding as a remaining hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.