IndisputableMonolith.Information.ErrorCorrectionBounds
The ErrorCorrectionBounds module formalizes Shannon channel capacity for binary symmetric channels and derives associated error correction bounds inside the Recognition Science 8-tick structure. It translates J-cost entropy into the classic C = 1 - H(p) expression and specializes it to discrete tick phases. Information theorists working on discrete or quantum models would cite the module for capacity limits and Hamming-style bounds. The module composes its results directly from the three imported upstream modules via algebraic substitution.
claimFor a binary symmetric channel with crossover probability $p$, the capacity is $C = 1 - H_2(p)$ where $H_2(p) = -p log_2 p - (1-p) log_2 (1-p)$, allowing reliable transmission at any rate $R < C$. In the eight-tick setting this fixes the redundancy needed for codes that correct a fixed number of errors per block.
background
The module belongs to the Information domain and imports three upstream modules. Constants supplies the RS time quantum τ₀ = 1 tick. Foundation.EightTick supplies the discrete clock whose phases are 0, π/4, π/2, 3π/4, π, 5π/4, 3π/2, 7π/4. ShannonEntropy supplies the derivation of Shannon entropy from J-cost: “Shannon entropy H = -Σ p_i log(p_i) is the fundamental measure of information. It quantifies uncertainty, compression limits, and channel capacity.”
proof idea
The module is a collection of definitions and short theorems that substitute the binary-entropy formula into the eight-tick phases. It defines binarySymmetricCapacity and capacity_at_10_percent by direct transcription of the entropy expression, then obtains hamming_bound_8tick and singleton_bound_8tick by the same substitution. All steps are algebraic reductions; no inductive or tactic-heavy arguments appear.
why it matters in Recognition Science
The module supplies the capacity and bound primitives required by the sibling declarations quantumErrorCorrection, topologicalCodes, toricCode and eight_tick_corrects_3. It realizes the channel-capacity statement of the DOC_COMMENT inside the eight-tick octave (T7) and thereby connects J-cost entropy to concrete error-correction limits in the Recognition framework.
scope and limits
- Does not derive the J-cost functional equation.
- Does not treat continuous or non-binary channels.
- Does not prove achievability of the capacity bound.
- Does not connect to spatial dimension or mass-ladder formulas.
depends on (3)
declarations in this module (18)
-
def
binarySymmetricCapacity -
def
capacity_at_10_percent -
structure
ErrorCode -
theorem
hamming_bound_8tick -
theorem
singleton_bound_8tick -
theorem
eight_tick_redundancy -
def
eightTickCode -
theorem
eight_tick_corrects_3 -
def
quantumErrorCorrection -
theorem
threshold_majority_voting -
def
topologicalCodes -
def
toricCode -
def
eightTickSyndrome -
theorem
detect_vs_correct -
theorem
rate_bound_from_8_tick -
theorem
error_bound_from_8_tick -
def
summary -
structure
ErrorCorrectionFalsifier