IndisputableMonolith.Information.PolarCodeGapFromPhi

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Polar Code Gap-to-Capacity on the Phi-Ladder
   6
   7Polar codes (Arıkan 2009) achieve Shannon capacity with gap decaying as
   8`O(2^{-N^{0.5}})` in block length N. In RS terms, the finite-length
   9gap-to-capacity for polar codes sits on the φ-ladder: adjacent-N-level
  10gaps ratio by `1/φ`. This is the same `1/φ` structure as the quantum-
  11channel-capacity correction (`Information/QuantumChannelCapacityFromPhi`)
  12and the LDPC code-rate gap.
  13
  14Lean status: 0 sorry, 0 axiom.
  15-/
  16
  17namespace IndisputableMonolith
  18namespace Information
  19namespace PolarCodeGapFromPhi
  20
  21open Constants
  22
  23noncomputable section
  24
  25/-- Reference polar code gap at rung 0 (minimal block length). -/
  26def referenceGap : ℝ := 1
  27
  28/-- Gap-to-capacity at φ-ladder rung `k`. -/
  29def gapAt (k : ℕ) : ℝ := referenceGap * phi ^ (-(k : ℤ))
  30
  31theorem gapAt_pos (k : ℕ) : 0 < gapAt k := by
  32  unfold gapAt referenceGap
  33  have : 0 < phi ^ (-(k : ℤ)) := zpow_pos Constants.phi_pos _
  34  linarith [this]
  35
  36theorem gapAt_succ_ratio (k : ℕ) :
  37    gapAt (k + 1) = gapAt k * phi⁻¹ := by
  38  unfold gapAt
  39  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  40  have : phi ^ (-((k : ℤ) + 1)) = phi ^ (-(k : ℤ)) * phi⁻¹ := by
  41    rw [show (-((k : ℤ) + 1)) = -(k : ℤ) + (-1 : ℤ) by ring]
  42    rw [zpow_add₀ hphi_ne]; simp
  43  have hcast : ((k + 1 : ℕ) : ℤ) = (k : ℤ) + 1 := by push_cast; ring
  44  rw [hcast, this]; ring
  45
  46theorem gapAt_adjacent_ratio (k : ℕ) :
  47    gapAt (k + 1) / gapAt k = phi⁻¹ := by
  48  rw [gapAt_succ_ratio]
  49  field_simp [(gapAt_pos k).ne']
  50
  51structure PolarCodeCert where
  52  gap_pos : ∀ k, 0 < gapAt k
  53  one_step_ratio : ∀ k, gapAt (k + 1) = gapAt k * phi⁻¹
  54  adjacent_ratio : ∀ k, gapAt (k + 1) / gapAt k = phi⁻¹
  55
  56/-- Polar-code gap-to-capacity certificate. -/
  57def polarCodeCert : PolarCodeCert where
  58  gap_pos := gapAt_pos
  59  one_step_ratio := gapAt_succ_ratio
  60  adjacent_ratio := gapAt_adjacent_ratio
  61
  62end
  63end PolarCodeGapFromPhi
  64end Information
  65end IndisputableMonolith
  66