ShannonAsJCostLimitCert
plain-language theorem explainer
The ShannonAsJCostLimitCert structure packages four algebraic properties of the finite-N correction to classical Shannon capacity: non-negativity for N>0, exact value at N=1, strict bounds 0<correction<1 at N=1, and the decomposition C_RS = C_classical minus correction. Information theorists working on finite-blocklength regimes would cite it to justify the explicit 1/phi correction in the RS model. The structure is inhabited by a one-line constructor that applies the supporting lemmas correction_RS_nonneg, correction_RS_at_one, correction_RS_1
Claim. Let $C_mathrm{classical}(N) := log_2 N$ and let $delta(N) := log_2(1 + 1/(phi N))$. The certificate asserts that $delta(N) geq 0$ for every $N>0$, that $delta(1) = log_2(1 + 1/phi)$, that $0 < delta(1) < 1$, and that the RS capacity satisfies $C_mathrm{RS}(N) = C_mathrm{classical}(N) - delta(N)$ for all $N$.
background
The module recovers the classical Shannon channel capacity $C = log_2 N$ as the high-N limit of J-cost on a message ensemble. At finite N the RS model supplies the explicit correction $delta(N) = log_2(1 + 1/(phi N))$, so that $C_mathrm{RS}(N) = log_2 N - delta(N)$. The Constants structure imported from LawOfExistence supplies the golden-ratio value phi together with the other CPM constants. Upstream results establish that the correction is non-negative and that its value at N=1 lies strictly between 0 and 1.
proof idea
The declaration is a structure definition that packages four properties of the correction term. It is inhabited by the one-line constructor shannonAsJCostLimitCert, which supplies the lemmas correction_RS_nonneg for non-negativity, correction_RS_at_one for the exact value at unity, correction_RS_one_band for the strict inequalities at N=1, and reflexivity for the decomposition identity.
why it matters
This certificate supplies the algebraic backbone for the finite-N Shannon capacity formula in Track F7 and is directly used by the inhabiting definition shannonAsJCostLimitCert. It closes the algebraic part of the claim that the RS correction vanishes in the high-N limit while remaining positive and bounded at N=1, consistent with the J-uniqueness and phi-ladder landmarks of the Recognition framework. The module doc-comment notes that the empirical match for finite-N coding is left as a hypothesis; the certificate itself is a theorem with zero sorry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.