pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Information.ErrorCorrectionBounds

show as:
view Lean formalization →

The module formalizes Shannon channel capacity for binary symmetric channels by deriving binary entropy from the J-cost and embedding results in the eight-tick discrete clock. Researchers in discrete spacetime physics cite it to establish reliable transmission rates R below capacity C = 1 - H(p). It consists of definitions for error codes and bounds like the Hamming bound adapted to the 8-tick structure, relying on algebraic application of upstream entropy lemmas.

claimFor a binary symmetric channel with crossover probability $p$, the capacity is $C = 1 - H_2(p)$ where the binary entropy $H_2(p) = -p log_2 p - (1-p) log_2 (1-p)$ is obtained from the J-cost. Reliable communication is possible at any rate $R < C$.

background

Recognition Science operates on an 8-tick discrete clock with phases at multiples of $pi/4$ and fundamental time quantum $tau_0 = 1$ tick. The upstream ShannonEntropy module derives entropy $H = -sum p_i log p_i$ directly from the J-cost structure as the measure of uncertainty. This module applies those primitives to error correction, introducing types such as ErrorCode and eightTickCode that respect the discrete phases.

proof idea

This is a definition module, no proofs. It declares supporting types including ErrorCode and eightTickCode, then states theorems such as hamming_bound_8tick and singleton_bound_8tick that apply the binary entropy definition to derive code size limits in the eight-tick setting.

why it matters in Recognition Science

It supplies the capacity and bound results that support quantumErrorCorrection and topologicalCodes within the module. The content realizes the Shannon capacity theorem for the binary symmetric channel, tying it to the eight-tick octave in the forcing chain. This step grounds information limits in Recognition Science primitives, enabling thresholds for error correction in discrete models.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (18)