Information Error Correction Codes From Jcost Threshold Gap Pos

The threshold gap

In information theory, the Shannon limit sets the maximum rate at which data can be transmitted reliably over a noisy channel. Real error-correcting codes operate below this limit, and the difference between a code's achievable rate and the Shannon limit is its threshold gap, a measure of how far the code is from ideal efficiency. The Recognition Science framework models five canonical code families, repetition, Hamming, BCH/Reed-Solomon, LDPC, and polar, as a ladder of decreasing threshold gaps.

The declaration thresholdGap_pos establishes a basic property of this ladder: for every natural number k, the gap defined as 1 divided by the golden ratio raised to the k-th power is strictly positive. In plain terms, it proves that the gap is always a positive number, never zero and never negative. The companion theorem thresholdGap_strictDecr shows that as k increases, the gap strictly decreases, meaning each rung on the ladder is closer to the Shannon limit than the one before. These are simple consequences of the golden ratio being greater than one.

The framework's library, a machine-checked collection of formal theorems, proves these statements with no unverified assumptions. The five-family count and the positivity and monotonicity of the gap are bundled into a certificate structure that the library constructs. This gives a formal guarantee that the ladder's ordering is consistent: deeper families, with smaller gaps, are strictly closer to capacity.

What the declaration does not claim is equally important. It does not assert that any real-world code achieves these rates, nor does it specify which physical codes belong to which family. The mapping from the five abstract families to actual coding schemes is a modeling choice, not a theorem. The threshold gap being positive does not imply that a code with that gap is decodable in practice; it only describes a mathematical relationship between the gap and the golden ratio ladder.

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

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

What this page does not claim

No claim that any real-world code achieves a rate corresponding to a threshold gap on the ladder. No claim that the mapping from abstract families to actual coding schemes is proven, only modeled. No claim that a positive threshold gap implies decodability in practice.

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: