Information Error Correction Codes From Jcost Threshold Gap Strict Decr

The threshold gap ladder

Error-correcting codes add redundancy to messages so that noise can be detected and fixed. Claude Shannon's 1948 theorem set the maximum rate at which information can travel through a noisy channel, the Shannon limit. A code's rate is the fraction of the transmitted bits that carry actual message; the gap to the limit is 1 minus that rate. The smaller the gap, the closer a code operates to the theoretical maximum, and the harder decoding becomes.

In the Recognition Science framework, five canonical error-correction families, repetition, Hamming, BCH/Reed-Solomon, LDPC, and polar codes, are modeled as occupying successive rungs of a ladder. The framework defines the threshold gap, a discrete record of how far a family sits from the Shannon limit, as 1 divided by the golden ratio raised to a step count. The golden ratio, about 1.618, is the number the framework's forcing chain derives as the unique self-similar scaling. The gap at step k is 1 / φ^k.

The declaration thresholdGap_strictDecr proves that this gap strictly decreases at every step: thresholdGap (k + 1) < thresholdGap k. In plain language, each deeper family on the ladder is strictly closer to the Shannon limit than the one before it. The proof is machine-checked in the framework's library of formal theorems, with no unproved assumptions. The same library also proves the gap is always positive, and packages both facts with the count of five families into a single certificate.

The theorem does not claim that any particular code reaches the Shannon limit, or that the five named families are the only possible ones. It establishes a strict ordering of the gaps, not their absolute values. The framework's docstring adds a separate, unformalized claim that a rate r is decodable if a certain cost expression falls below a canonical band; that claim is not part of the theorem and is not proved in Lean.

theorem thresholdGap_strictDecr (k : ℕ) :
    thresholdGap (k + 1) < thresholdGap k := by
  unfold thresholdGap
  have hpos_k : (0 : ℝ) < phi ^ k := pow_pos phi_pos k
  have h_growth : phi ^ k < phi ^ (k + 1) := by
    rw [pow_succ]
    have h1 : 1 < phi := one_lt_phi
    nlinarith
  exact one_div_lt_one_div_of_lt hpos_k h_growth

theorem thresholdGap_pos (k : ℕ) : 0 < thresholdGap k := by
  unfold thresholdGap
  exact div_pos one_pos (pow_pos phi_pos k)

noncomputable def eccCert : ECCCert where
  five_families := eccFamily_count
  threshold_always_pos := thresholdGap_pos
  threshold_strictly_decreasing := thresholdGap_strictDecr

What this page does not claim

The theorem does not claim that any real code achieves the Shannon limit. The theorem does not claim the five named families are exhaustive. The decodability condition involving the canonical band J(φ) is stated in a docstring, not proved in Lean.

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/ErrorCorrectionCodesFromJCost.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: