Information Error Correction Bounds Singleton Bound 8tick

The Singleton bound in eight ticks

The Singleton bound is a fundamental limit in coding theory. It states that for any error-correcting code with codewords of length n, message length k, and minimum distance d, the inequality n ≤ n - d + 1 must hold. This bound, named after Richard Singleton who published it in 1964, gives the maximum possible minimum distance for a code with given length and dimension. Codes that meet this bound exactly are called maximum distance separable (MDS) codes, and they are optimal in a precise sense: they achieve the greatest possible error correction for their size.

The theorem named singleton_bound_8tick in the framework's machine-checked library of formal theorems establishes that a specific code satisfies this bound. The code in question is defined as eightTickCode, which has eight symbols (n = 8), one message bit (k = 1), and minimum distance eight (d = 8). The theorem proves the inequality 8 ≤ 8 - 1 + 1, which simplifies to 8 ≤ 8. This is a trivial arithmetic fact, but its significance lies in what it represents: a formal verification that the eight-tick code meets the Singleton bound.

In the Recognition Science framework, the eight-tick structure comes from a derived recognition cycle. The framework models information as being encoded across eight phases or ticks, providing natural redundancy. The code's parameters mean it can detect up to seven errors (d - 1 = 7) and correct up to three errors, as shown by the theorem (d - 1) / 2 = 3. This aligns with majority voting: with eight copies of one bit, a majority vote can correct any three flipped bits. The framework also proves a Hamming bound for this code, showing that 2^1 × (C(8,0) + C(8,1) + C(8,2) + C(8,3)) ≤ 2^8, which confirms the code is within the sphere-packing limit.

What the theorem does not claim is more interesting than what it proves. The Singleton bound is a necessary condition, not a sufficient one. Satisfying it does not mean the code is good, practical, or even exists as a useful error-correcting code. The theorem does not prove that the eight-tick code achieves channel capacity, nor does it show that eight ticks are the optimal or only way to encode information. The framework's own docstring notes that Shannon's channel capacity theorem gives the maximum reliable transmission rate, and the eight-tick code's rate of 1/8 is far below what is theoretically possible on a binary symmetric channel.

The declaration is best understood as a consistency check. It verifies that a code arising from the framework's eight-tick structure satisfies a classical bound from information theory. This is a small but real connection between the framework's derived structure and established coding theory. The theorem is proved by simple arithmetic (norm_num in the Lean proof assistant), reflecting that the mathematical content is elementary. The value is in the formal verification, not in discovering a new bound. The framework's library shows that the eight-tick code, with its specific parameters, is a legitimate error-correcting code by the standards of classical coding theory.

For a reader encountering this declaration, the takeaway is modest but concrete. The eight-tick code is a real code with defined parameters, and those parameters satisfy the Singleton bound. This means the code is not ruled out by this particular limit. It can detect up to seven errors and correct up to three, which is a genuine but limited capability. The framework does not claim this code is optimal, practical, or competitive with modern codes like LDPC or turbo codes. It claims only that this particular code, derived from the eight-tick structure, is consistent with a fundamental bound in information theory.

/-- The Singleton bound: d ≤ n - k + 1.

    Codes meeting this bound are MDS (Maximum Distance Separable).

    Formalized for the 8-tick code: d=8 ≤ 8-1+1 = 8. -/
theorem singleton_bound_8tick :
    (8 : ℕ) ≤ 8 - 1 + 1 := 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

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

What this page does not claim

The theorem does not prove the eight-tick code is optimal or achieves channel capacity. The Singleton bound is necessary but not sufficient for a good code; the theorem does not establish practical usefulness. The framework does not claim that eight ticks are the only or best way to structure error-correcting 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: