Pith. sign in
module module high

IndisputableMonolith.Information.ShannonAsJCostLimit

show as:
view Lean formalization →

This module introduces the classical Shannon channel capacity as the high-N limit of the Recognition Science J-cost formulation. Researchers recovering standard information bounds inside the monolith would cite the definitions when passing to the classical regime. The module supplies the base capacity expression together with a finite-N correction term whose vanishing is proved downstream.

claimThe classical Shannon channel capacity is $C = \log_2 N$ (in bits), recovered exactly as the limit of the RS cost-based capacity when the number of states $N \to \infty$.

background

The module sits in the Information domain and imports Constants, where the fundamental RS time quantum is defined as $\tau_0 = 1$ tick, together with the Cost module that supplies the J-cost structure. It introduces the classical capacity expression alongside the RS correction $\mathrm{correction_{RS}}(N) = \log_2(1 + 1/(\phi N))$. The setting prepares the high-N limit argument that recovers ordinary Shannon theory from the Recognition Science monolith.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the base objects for the ShannonHighNLimit theorem, which proves that the RS finite-N correction tends to zero as $N \to \infty$ and thereby recovers the classical Shannon capacity exactly. It corresponds to the Track E5 deepening of Plan v5.

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)