pith. sign in
module module high

IndisputableMonolith.Information.ShannonAsJCostLimit

show as:
view Lean formalization →

The module sets up the classical Shannon channel capacity as the RS J-cost limit in the high-N regime. Researchers connecting information theory to Recognition Science cost structures would cite it as the base layer for finite-N corrections. The module imports the RS time quantum and cost primitives to declare C_classical and related correction terms without carrying out the limit argument itself.

claimThe classical Shannon channel capacity is $C = log_2 N$ bits, with $N$ the number of states and the underlying time unit the RS-native tick $τ_0 = 1$.

background

The module sits in the Information domain and imports the fundamental RS time quantum $τ_0 = 1$ tick from Constants together with cost primitives from the Cost module. It positions the classical capacity against RS-native J-cost expressions that incorporate the golden ratio $φ$ through finite-N correction terms. The setting prepares the comparison between the standard Shannon formula and its RS-adjusted counterparts on the phi-ladder.

proof idea

This is a definition module, no proofs. It declares C_classical together with correction_RS and supporting non-negativity and boundary lemmas that are invoked by the downstream high-N limit argument.

why it matters in Recognition Science

The module supplies the base definitions for the ShannonHighNLimit theorem, which proves that the RS correction $correction_RS(N) = log_2(1 + 1/(φ·N))$ vanishes as $N → ∞$ and thereby recovers the exact classical capacity $C(N) = log_2 N$. It corresponds to Track E5 of Plan v5 for the information-theoretic foundations.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (9)