Information Error Correction Bounds Hamming Bound 8tick

The eight-tick bound

Error correction is the art of adding redundancy so that noise can be undone. A simple code might send each message bit three times and let the receiver vote; two agreeing copies outvote one corrupted one. The Hamming bound is a classical limit on how much redundancy any code must carry: it says that for a code of length n that corrects t errors, the number of codewords cannot exceed 2^n divided by the number of error patterns within distance t of a codeword. The bound does not say such a code exists, only that no code can beat it.

The framework's machine-checked library of formal theorems contains a declaration, hamming_bound_8tick, that instantiates this classical bound for a specific code. The code has length 8, message length 1, and minimum distance 8, written as eightTickCode. The theorem states that 2^1 times the sum of binomial coefficients (8 choose 0 through 8 choose 3) is at most 2^8. In plain terms, a code with eight positions and one message bit, designed to correct up to three errors, satisfies the Hamming bound. The proof is a direct numeric check, not a deep structural argument.

What the declaration actually proves is arithmetic about this one code. It shows that the bound holds: the left side, 2 * (1 + 8 + 28 + 56) = 186, is indeed less than 256. It also proves, in a separate theorem, that the code's minimum distance of 8 allows it to correct up to 3 errors, since (8 - 1) / 2 = 3. These are exact statements about the code's parameters, verified by computation.

The declaration does not claim that the code exists in any physical sense, nor that it is optimal, nor that it achieves the bound. It does not show that eight phases in the Recognition Science framework correspond to a working error-correcting code in a real channel. The theorem is a consistency check: a particular code with these parameters respects the classical limit. It leaves open whether the framework's eight-tick structure can actually be realized as a code that corrects errors in practice.

What the result changes is the status of the eight-tick idea within the framework. Before the theorem, the claim that eight phases provide natural redundancy was a hope. After it, the claim is at least compatible with the fundamental bound of coding theory. The framework's library can point to a machine-checked proof that its proposed code does not violate the Hamming bound, which is a necessary condition for any serious error-correction scheme. It is a small but real step from an idea to a checkable statement.

/-- The Hamming bound (sphere-packing bound):

    For t-error-correcting code:
    2^k × Σᵢ₌₀ᵗ C(n,i) ≤ 2ⁿ

    Codes meeting this bound are "perfect" (e.g., Hamming codes).

    Formalized as: for our 8-tick code with d=8, t=3,
    the volume of radius-3 balls around 2^1 codewords fits inside {0,1}^8. -/
theorem hamming_bound_8tick :
    2 ^ 1 * (Nat.choose 8 0 + Nat.choose 8 1 +
      Nat.choose 8 2 + Nat.choose 8 3)
    ≤ 2 ^ 8 := by
  native_decide

theorem eight_tick_corrects_3 :
    -- 8-tick code corrects up to 3 errors
    (eightTickCode.d - 1) / 2 = 3 := by rfl

/-- 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⟩

What this page does not claim

The theorem does not prove that a code with these parameters exists. The theorem does not show that eight phases provide any real error-correction benefit in practice. The theorem does not establish any connection between the eight-tick structure and Shannon's channel capacity.

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: