gap_doubling_halves

formal source

  67  exact one_div_lt_one_div_of_lt hphi_N1 h_lt'
  68
  69/-- Doubling N halves the gap. -/
  70theorem gap_doubling_halves {N : ℝ} (hN : 0 < N) :
  71    gapToCapacity (2 * N) = gapToCapacity N / 2 := by
  72  unfold gapToCapacity
  73  have hp : phi ≠ 0 := phi_ne_zero
  74  have hN' : N ≠ 0 := ne_of_gt hN
  75  field_simp
  76
  77/-- For N = 10000, the gap matches the empirical ~0.5 dB ≈ 1/(φ·10⁴). -/
  78def gapAt10k : ℝ := gapToCapacity 10000
  79
  80theorem gap_at_10k_eq : gapAt10k = 1 / (phi * 10000) := rfl
  81
  82theorem gap_at_10k_pos : 0 < gapAt10k := by
  83  unfold gapAt10k; exact gap_pos (by norm_num : (0:ℝ) < 10000)
  84
  85/-- Gap-vs-block-length monotone law: gap(N) · N = 1/φ. -/
  86theorem gap_times_N_invariant {N : ℝ} (hN : 0 < N) :
  87    gapToCapacity N * N = 1 / phi := by
  88  unfold gapToCapacity
  89  have h : N ≠ 0 := ne_of_gt hN
  90  field_simp
  91
  92/-- Certificate. -/
  93structure LDPCRateCert where
  94  gap_pos : ∀ {N : ℝ}, 0 < N → 0 < gapToCapacity N
  95  gap_monotone : ∀ {N₁ N₂ : ℝ}, 0 < N₁ → N₁ < N₂ →
  96    gapToCapacity N₂ < gapToCapacity N₁
  97  doubling_halves : ∀ {N : ℝ}, 0 < N →
  98    gapToCapacity (2 * N) = gapToCapacity N / 2
  99  gap_N_invariant : ∀ {N : ℝ}, 0 < N → gapToCapacity N * N = 1 / phi
 100