C_classical
plain-language theorem explainer
C_classical supplies the classical Shannon channel capacity as the base-two logarithm of the symbol count N. Researchers deriving finite-N corrections within the Recognition Science J-cost formalism cite this as the high-N asymptotic target. The definition is a direct one-line abbreviation to the real logarithm base two.
Claim. The classical Shannon channel capacity in bits is given by $C(N) = log_2 N$.
background
This definition sits in the module on Shannon Entropy as J-Cost Limit (Track F7). The module recovers the classical capacity as the high-N limit of J-cost on the message ensemble, with the RS finite-N capacity obtained by subtracting a phi-ladder correction of the form log₂(1 + 1/(φ N)). The upstream correction from QuantumChannelCapacityFromPhi is defined as 1/(phi * N) for positive integer N and is strictly positive at every such N. C_classical therefore serves as the reference baseline before the module defines C_RS(N) = C_classical(N) - correction_RS(N) and assembles the master certificate collecting non-negativity, bandedness at N=1, and decomposition.
proof idea
The declaration is a direct definition that unfolds immediately to Real.logb 2 N. No lemmas are invoked and no tactics are applied; it functions as the foundational abbreviation for the classical limit used in all subsequent ring equalities and limit arguments.
why it matters
This definition anchors the Shannon-as-J-Cost-Limit master certificate (Track F7). It is referenced by the decomposition theorem C_classical_minus_C_RS_eq_correction, which states that the RS capacity gap equals the correction term, and by the ShannonAsJCostLimitCert structure that collects non-negativity, the explicit value at N=1, and the decomposition identity. In the Recognition framework it marks the high-N limit step where the correction tends to zero, recovering standard Shannon capacity from the J-cost formalism and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.