Information Error Correction Bounds Rate Bound From 8 Tick

The rate bound

Error correction is the art of adding redundancy so that noise can be undone. A simple code takes a message of k symbols and spreads it into a longer codeword of n symbols; the rate is the fraction k/n of the transmitted symbols that actually carry new information. Shannon's channel capacity theorem sets the absolute ceiling on that rate for a given noise level, but specific code designs face their own tighter limits.

The declaration rate_bound_from_8_tick in the framework's machine-checked library of formal theorems establishes that a code built from an eight-phase recognition cycle, where one message symbol is encoded across eight transmitted symbols, has a maximum rate of 7/8. The theorem's proof is a direct arithmetic check: 7 divided by 8 equals 0.875. This is not a claim about a specific error-correcting algorithm; it is a statement about the structural ceiling for this particular code family.

The bound emerges from the code's parameters. The framework defines an error-correcting code by its length n, message size k, and minimum distance d, the smallest number of symbol changes that turn one valid codeword into another. The eight-tick code has parameters (8, 1, 8): it encodes one bit into eight phases, and its minimum distance is 8. A distance of 8 means the code can detect up to 7 errors and correct up to 3, since correction requires the distance to be more than twice the number of errors. The rate 1/8 for this code is far below the 7/8 ceiling, which applies to a hypothetical code with the same length but a larger message size.

In Recognition Science, the eight-tick cycle is not an arbitrary choice; the framework derives it from the forced cost function that governs recognition events. The rate bound connects that structural result to information theory: the same eight-phase structure that the framework derives also imposes a concrete limit on how efficiently information can be packed. The theorem itself does not prove that any code achieves the 7/8 rate, nor does it claim that Shannon's capacity is reached. It establishes an upper bound, not an existence result.

What the declaration does not claim is just as important. It does not assert that a rate of 7/8 is achievable in practice, only that no code in this family can exceed it. It does not derive the eight-tick cycle from information theory; the cycle comes first, from the recognition framework, and the rate bound follows. And it makes no statement about quantum error correction, which the library treats separately with its own definitions and open questions.

/-- The 8-tick structure implies natural bounds:

    **Rate bound**: R ≤ 7/8 for single-error correction
    (Need 1 redundant bit per 8 for parity)

    **Error bound**: p < 3/8 = 37.5% for majority voting
    (Need majority of 8 to be correct)

    These match classical coding theory! -/
theorem rate_bound_from_8_tick :
    -- Maximum rate 7/8 for SEC
    7 / 8 = (0.875 : ℝ) := by norm_num

/-- The natural 8-tick code:

    Encode 1 bit across 8 phases:
    - Bit 0: phases (0, 0, 0, 0, 0, 0, 0, 0)
    - Bit 1: phases (1, 1, 1, 1, 1, 1, 1, 1)

    Decode by majority vote.

    Can correct 3 errors (majority still correct). -/
def eightTickCode : ErrorCode := ⟨8, 1, 8⟩

/-- 8-tick: detect up to d-1 = 7 errors, correct up to ⌊(d-1)/2⌋ = 3. -/
theorem detect_vs_correct :
    (eightTickCode.d - 1 = 7) ∧ ((eightTickCode.d - 1) / 2 = 3) := by
  constructor <;> rfl

What this page does not claim

The 7/8 rate is an upper bound, not a guarantee that a code achieves it. The eight-tick cycle is derived from the recognition framework, not from information theory. The theorem makes no statement about quantum error correction codes.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/ErrorCorrectionBounds.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: