pith. sign in
module module high

IndisputableMonolith.Information.ErrorCorrectionBounds

show as:
view Lean formalization →

This module assembles error-correction bounds for binary symmetric channels inside the Recognition Science eight-tick clock by importing Shannon entropy derived from J-cost. Information theorists working on discrete physical channels would cite the capacity formula and the adapted Hamming and singleton bounds. The module is a collection of definitions and statements that restate classical results in RS-native units without new derivations.

claimFor a binary symmetric channel with crossover probability $p$, the capacity is $C=1-H(p)$ where $H(p)=-p\log_2 p-(1-p)\log_2(1-p)$ is the binary entropy; reliable transmission is possible at any rate $R<C$. The module also states the Hamming bound and singleton bound specialized to eight-tick codes.

background

The module operates in the Information domain and imports three upstream modules. Constants supplies the fundamental time quantum $\tau_0=1$ tick. EightTick defines the discrete 8-tick cycle with phases $0,\pi/4,\pi/2,3\pi/4,\pi,5\pi/4,3\pi/2,7\pi/4$. ShannonEntropy states that Shannon entropy $H=-\sum p_i\log p_i$ arises directly from the J-cost structure of Recognition Science.

The supplied doc-comment reproduces Shannon's channel-capacity theorem for the binary symmetric channel and notes that any rate below capacity permits reliable transmission. Sibling declarations inside the module (binarySymmetricCapacity, hamming_bound_8tick, eight_tick_redundancy, etc.) translate these classical statements into the eight-tick setting.

proof idea

This is a definition module, no proofs. It simply records the classical capacity formula, the binary-symmetric-channel specialization, and the standard Hamming and singleton bounds after substituting the eight-tick period and J-cost entropy.

why it matters in Recognition Science

The module supplies the information-theoretic layer required by the eight-tick octave (T7) before error-correction arguments can be applied to physical codes. It feeds the sibling declarations that define eightTickCode, topologicalCodes and toricCode, thereby linking Shannon capacity to the discrete clock structure. No downstream theorems are recorded yet; the module therefore closes the interface between the ShannonEntropy import and concrete coding bounds.

scope and limits

depends on (3)

Lean names referenced from this declaration's body.

declarations in this module (18)