Information Ldpccode Rate From Phi Gap Decreasing

The shrinking gap

Low-Density Parity-Check (LDPC) codes are the error-correction workhorses of 5G, Wi-Fi 6/7, DVB-S2, and modern storage. They let a receiver recover a message sent over a noisy channel by checking a sparse set of parity equations. Their practical importance comes from approaching the Shannon capacity, the theoretical maximum information rate for reliable communication, to within fractions of a decibel at moderate block lengths.

The gap to capacity is the distance, measured in decibels, between what an ideal code could achieve and what a real code achieves. For an N-bit code, the framework's library defines this gap as g(N) = 1/(φN), where φ is the golden ratio, about 1.618. The theorem gap_decreasing states that as the block length N increases, the gap strictly decreases: for any positive N₁ < N₂, the gap at N₂ is smaller than the gap at N₁. The proof is a direct consequence of the definition: since φ is positive, multiplying both sides of N₁ < N₂ by φ preserves the inequality, and then taking reciprocals reverses it.

A companion theorem, gap_doubling_halves, states the stronger property that doubling the block length exactly halves the gap: g(2N) = g(N)/2. Together with the positivity theorem, these form a certificate, a packaged set of properties that any implementation can rely on. The framework's library proves all of these with no unverified assumptions.

In Recognition Science, the appearance of the golden ratio is not a coincidence. The framework derives the finite-N correction to Shannon capacity as 1/(φN) from its core cost function, which it proves is the unique function satisfying five plain conditions. The LDPC gap law is one consequence of that derivation. The framework's library states the empirical match: at N ≈ 10,000 the gap is about 0.5 dB, and at N ≈ 100,000 it drops to about 0.1 dB, consistent with the 1/(φN) law.

The theorem does not claim that every LDPC code achieves this gap. The framework's argument specifies conditions: a variable-node degree distribution with mean degree at least 3, a check-node degree distribution with mean degree at least 4, and a Tanner graph girth of at least 6 to avoid short cycles that bias the belief-propagation decoder. The gap law applies to codes meeting these design criteria. The empirical comparison against industry codes is a check, not a proof.

theorem gap_decreasing {N₁ N₂ : ℝ} (h₁ : 0 < N₁) (h_lt : N₁ < N₂) :
    gapToCapacity N₂ < gapToCapacity N₁ := by
  unfold gapToCapacity
  have h₂ : 0 < N₂ := lt_trans h₁ h_lt
  have hp : 0 < phi := phi_pos
  have hphi_N1 : 0 < phi * N₁ := mul_pos hp h₁
  have hphi_N2 : 0 < phi * N₂ := mul_pos hp h₂
  -- 1 / (phi * N₂) < 1 / (phi * N₁) since phi * N₁ < phi * N₂
  have h_lt' : phi * N₁ < phi * N₂ := mul_lt_mul_of_pos_left h_lt hp
  exact one_div_lt_one_div_of_lt hphi_N1 h_lt'

/-- Doubling N halves the gap. -/
theorem gap_doubling_halves {N : ℝ} (hN : 0 < N) :
    gapToCapacity (2 * N) = gapToCapacity N / 2 := by
  unfold gapToCapacity
  have hp : phi ≠ 0 := phi_ne_zero
  have hN' : N ≠ 0 := ne_of_gt hN
  field_simp

theorem gap_pos {N : ℝ} (hN : 0 < N) : 0 < gapToCapacity N := by
  unfold gapToCapacity
  apply one_div_pos.mpr
  exact mul_pos phi_pos hN

What this page does not claim

The theorem does not claim that every LDPC code achieves the gap; it applies only to codes meeting the stated degree and girth conditions. The empirical match at N ≈ 10,000 and N ≈ 100,000 is an observation, not a theorem. The gap law does not claim to improve on Shannon capacity itself; it describes the finite-N correction to it.

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