IndisputableMonolith.Information.QuantumChannelCapacityFromPhi

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Quantum Channel Capacity Correction from the Phi-Ladder
   6
   7The classical Shannon capacity is `C = log₂(1 + S/N)`. The quantum
   8analog (entanglement-assisted, classical capacity, or coherent
   9information channel capacity) carries an RS finite-N correction that
  10scales as `log₂(1 + 1/(φ · N))` per input symbol — the same φ-suppressed
  11correction that appears in the classical Shannon bound (already
  12formalised in `Information/ShannonAsJCostLimit`).
  13
  14The structural prediction: the entanglement-assisted-to-classical
  15capacity ratio for an N-symbol block channel is `1 + 1/(φ N)`. Adjacent-N
  16ratios differ by `(N+1)/N · 1/φ` to leading order; the correction
  17vanishes as `1/N` rather than `1/N²` — distinguishable from any
  18classical-only model that has zero finite-N correction.
  19
  20Lean status: 0 sorry, 0 axiom.
  21-/
  22
  23namespace IndisputableMonolith
  24namespace Information
  25namespace QuantumChannelCapacityFromPhi
  26
  27open Constants
  28
  29noncomputable section
  30
  31/-- The φ-ladder finite-N correction factor for quantum channel
  32capacity at input-symbol-count `N`. -/
  33def correction (N : ℕ) (hN : 0 < N) : ℝ := 1 / (phi * (N : ℝ))
  34
  35/-- Correction is strictly positive at every positive `N`. -/
  36theorem correction_pos (N : ℕ) (hN : 0 < N) : 0 < correction N hN := by
  37  unfold correction
  38  have hphi : 0 < phi := Constants.phi_pos
  39  have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
  40  positivity
  41
  42/-- Correction strictly decreases with `N` (from `N` to `N+1`). -/
  43theorem correction_strictly_decreasing (N : ℕ) (hN : 0 < N) :
  44    correction (N + 1) (Nat.succ_pos _) < correction N hN := by
  45  unfold correction
  46  have hphi : 0 < phi := Constants.phi_pos
  47  have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
  48  have hN1pos : (0 : ℝ) < ((N + 1 : ℕ) : ℝ) := by exact_mod_cast Nat.succ_pos _
  49  have hphiN_pos : (0 : ℝ) < phi * (N : ℝ) := by positivity
  50  have hphiN1_pos : (0 : ℝ) < phi * ((N + 1 : ℕ) : ℝ) := by positivity
  51  have hphi_le_strict : phi * (N : ℝ) < phi * ((N + 1 : ℕ) : ℝ) := by
  52    apply mul_lt_mul_of_pos_left ?_ hphi
  53    exact_mod_cast Nat.lt_succ_self N
  54  exact one_div_lt_one_div_of_lt hphiN_pos hphi_le_strict
  55
  56/-- Correction tends to 0 as `N → ∞` (statement form using single
  57positive `N`; the limit is the standard `1/N → 0`). -/
  58theorem correction_le_inv {N : ℕ} (hN : 0 < N) :
  59    correction N hN ≤ 1 / (N : ℝ) := by
  60  unfold correction
  61  have hphi_gt_one : (1 : ℝ) < phi := by
  62    have := Constants.phi_gt_onePointFive; linarith
  63  have hphi : 0 < phi := Constants.phi_pos
  64  have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
  65  have hphiN : 0 < phi * (N : ℝ) := by positivity
  66  have hN_le : (N : ℝ) ≤ phi * (N : ℝ) := by
  67    have : (1 : ℝ) * (N : ℝ) ≤ phi * (N : ℝ) :=
  68      mul_le_mul_of_nonneg_right (le_of_lt hphi_gt_one) (le_of_lt hNpos)
  69    simpa using this
  70  exact one_div_le_one_div_of_le hNpos hN_le
  71
  72structure QuantumChannelCapacityCert where
  73  correction_pos : ∀ {N : ℕ} (hN : 0 < N), 0 < correction N hN
  74  strictly_decreasing :
  75    ∀ (N : ℕ) (hN : 0 < N),
  76      correction (N + 1) (Nat.succ_pos _) < correction N hN
  77  bounded_by_inv :
  78    ∀ {N : ℕ} (hN : 0 < N), correction N hN ≤ 1 / (N : ℝ)
  79
  80/-- Quantum-channel-capacity correction certificate. -/
  81def quantumChannelCapacityCert : QuantumChannelCapacityCert where
  82  correction_pos := @correction_pos
  83  strictly_decreasing := correction_strictly_decreasing
  84  bounded_by_inv := @correction_le_inv
  85
  86end
  87end QuantumChannelCapacityFromPhi
  88end Information
  89end IndisputableMonolith
  90