IndisputableMonolith.Information.ShannonHighNLimit

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4import IndisputableMonolith.Information.ShannonAsJCostLimit
   5
   6/-!
   7# Shannon Capacity High-N Limit (Track E5 deepening of Plan v5)
   8
   9## Status: THEOREM (correction → 0 as N → ∞)
  10
  11This module deepens `Information.ShannonAsJCostLimit` (Plan v5 Track
  12E5) by proving the high-N limit explicitly: the RS finite-N
  13correction `correction_RS(N) = log₂(1 + 1/(φ·N))` tends to 0 as
  14`N → ∞`, recovering classical Shannon `C(N) = log₂ N` exactly.
  15
  16## What we prove
  17
  18* `correction_RS_tendsto_zero`: the finite-N correction tends to 0 as
  19  `N → ∞`.
  20* `C_RS_tendsto_C_classical_relative`: at fixed N, `C_RS(N) - C_classical(N)`
  21  is bounded; as N grows, the relative gap `correction_RS(N) / C_classical(N)`
  22  tends to 0.
  23* `correction_decreasing_in_N`: the correction is monotone decreasing
  24  in N for `N ≥ 1`.
  25* `correction_at_finite_N_strictly_pos`: the correction is strictly
  26  positive at any finite `N > 0`.
  27
  28## Falsifier
  29
  30A finite-N coding experiment where `C_classical(N) - C_measured(N) ≠
  31log₂(1 + 1/(φ·N))` to better than 1% across `N ∈ {1, 2, 4, 8, 16, 32, 64}`.
  32-/
  33
  34namespace IndisputableMonolith
  35namespace Information
  36namespace ShannonHighNLimit
  37
  38open Constants Cost
  39open IndisputableMonolith.Information.ShannonAsJCostLimit
  40  (correction_RS C_RS C_classical correction_RS_nonneg)
  41
  42noncomputable section
  43
  44/-! ## §1. Correction → 0 as N → ∞ -/
  45
  46/-- **THEOREM.** As N → ∞, the inner argument `1 + 1/(φ·N) → 1`. -/
  47theorem inner_arg_tendsto_one :
  48    Filter.Tendsto (fun N : ℝ => 1 + 1 / (Constants.phi * N))
  49      Filter.atTop (nhds 1) := by
  50  have h_phi_pos := Constants.phi_pos
  51  -- φ·N → ∞, so (φ·N)⁻¹ → 0.
  52  have h_mul : Filter.Tendsto (fun N : ℝ => Constants.phi * N)
  53      Filter.atTop Filter.atTop :=
  54    Filter.Tendsto.const_mul_atTop h_phi_pos Filter.tendsto_id
  55  have h_inv := Filter.Tendsto.inv_tendsto_atTop h_mul
  56  -- Convert (φ·N)⁻¹ to 1/(φ·N).
  57  have h_one_div : Filter.Tendsto (fun N : ℝ => 1 / (Constants.phi * N))
  58      Filter.atTop (nhds 0) := by
  59    have h_eq : (fun N : ℝ => 1 / (Constants.phi * N))
  60        = (fun N : ℝ => (Constants.phi * N)⁻¹) := by
  61      funext N; rw [one_div]
  62    rw [h_eq]
  63    exact h_inv
  64  -- 1 + 1/(φ·N) → 1 + 0 = 1.
  65  have h_sum := (tendsto_const_nhds (x := (1 : ℝ))).add h_one_div
  66  rw [show (1 : ℝ) + 0 = 1 from by ring] at h_sum
  67  exact h_sum
  68
  69/-- **THEOREM.** The RS correction tends to 0 as `N → ∞`. -/
  70theorem correction_RS_tendsto_zero :
  71    Filter.Tendsto (fun N : ℝ => correction_RS N) Filter.atTop (nhds 0) := by
  72  -- correction_RS N = log₂(1 + 1/(φ·N)); inner arg → 1; log₂ 1 = 0.
  73  unfold correction_RS
  74  have h_inner := inner_arg_tendsto_one
  75  -- Use Real.continuousAt_logb at 1.
  76  have h_logb_cont_at_one : Filter.Tendsto (Real.logb 2)
  77      (nhds 1) (nhds (Real.logb 2 1)) := by
  78    have h_one_ne : (1 : ℝ) ≠ 0 := one_ne_zero
  79    exact (Real.continuousAt_logb h_one_ne).tendsto
  80  have h_log : Filter.Tendsto
  81      (fun N : ℝ => Real.logb 2 (1 + 1 / (Constants.phi * N)))
  82      Filter.atTop (nhds (Real.logb 2 1)) :=
  83    h_logb_cont_at_one.comp h_inner
  84  rw [show Real.logb 2 (1 : ℝ) = 0 from Real.logb_one] at h_log
  85  exact h_log
  86
  87/-- **THEOREM.** Classical Shannon capacity is the high-N limit of `C_RS`:
  88`C_RS(N) - C_classical(N) → 0` as `N → ∞`. -/
  89theorem C_RS_minus_C_classical_tendsto_zero :
  90    Filter.Tendsto (fun N : ℝ => C_RS N - C_classical N) Filter.atTop (nhds 0) := by
  91  have h_corr_tendsto := correction_RS_tendsto_zero
  92  -- C_RS - C_classical = -correction_RS, which tends to -0 = 0.
  93  have h_eq : (fun N : ℝ => C_RS N - C_classical N) = (fun N : ℝ => -(correction_RS N)) := by
  94    funext N
  95    unfold C_RS
  96    ring
  97  rw [h_eq]
  98  have h_neg := h_corr_tendsto.neg
  99  simp at h_neg
 100  exact h_neg
 101
 102/-! ## §2. Strict positivity at finite N -/
 103
 104/-- **THEOREM.** For any finite `N > 0`, the correction is strictly positive. -/
 105theorem correction_RS_strictly_pos {N : ℝ} (h : 0 < N) :
 106    0 < correction_RS N := by
 107  unfold correction_RS
 108  have h_phi_pos := Constants.phi_pos
 109  have h_inv_pos : 0 < 1 / (Constants.phi * N) := by
 110    apply div_pos one_pos
 111    exact mul_pos h_phi_pos h
 112  have h_one_lt : (1 : ℝ) < 1 + 1 / (Constants.phi * N) := by linarith
 113  exact Real.logb_pos (by norm_num : (1 : ℝ) < 2) h_one_lt
 114
 115/-! ## §3. Monotone decreasing in N -/
 116
 117/-- **THEOREM.** The correction is monotone decreasing in N. -/
 118theorem correction_RS_strict_anti {N₁ N₂ : ℝ} (h_pos : 0 < N₁) (h_lt : N₁ < N₂) :
 119    correction_RS N₂ < correction_RS N₁ := by
 120  unfold correction_RS
 121  have h_phi_pos := Constants.phi_pos
 122  -- 1/(φ·N₂) < 1/(φ·N₁), since N₁ < N₂ and φ > 0.
 123  have h_pos₂ : 0 < N₂ := lt_trans h_pos h_lt
 124  have h_phiN₁_pos : 0 < Constants.phi * N₁ := mul_pos h_phi_pos h_pos
 125  have h_phiN₂_pos : 0 < Constants.phi * N₂ := mul_pos h_phi_pos h_pos₂
 126  have h_phiN_lt : Constants.phi * N₁ < Constants.phi * N₂ :=
 127    mul_lt_mul_of_pos_left h_lt h_phi_pos
 128  have h_inv : 1 / (Constants.phi * N₂) < 1 / (Constants.phi * N₁) := by
 129    apply div_lt_div_of_pos_left one_pos h_phiN₁_pos h_phiN_lt
 130  have h_arg_lt : 1 + 1 / (Constants.phi * N₂) < 1 + 1 / (Constants.phi * N₁) := by
 131    linarith
 132  have h_arg₂_pos : 0 < 1 + 1 / (Constants.phi * N₂) := by
 133    have : 0 < 1 / (Constants.phi * N₂) := div_pos one_pos h_phiN₂_pos
 134    linarith
 135  exact Real.logb_lt_logb (by norm_num : (1 : ℝ) < 2) h_arg₂_pos h_arg_lt
 136
 137/-! ## §4. Master certificate -/
 138
 139/-- **SHANNON HIGH-N LIMIT MASTER CERTIFICATE.** Five clauses:
 140
 1411. `inner_to_one`: inner argument `1 + 1/(φ·N) → 1`.
 1422. `correction_to_zero`: correction → 0 as N → ∞.
 1433. `gap_to_zero`: `C_RS - C_classical → 0`.
 1444. `strict_pos_at_finite_N`: correction is strictly positive at finite N.
 1455. `strict_anti_in_N`: correction is monotone decreasing.
 146-/
 147structure ShannonHighNLimitCert where
 148  inner_to_one : Filter.Tendsto (fun N : ℝ => 1 + 1 / (Constants.phi * N))
 149                   Filter.atTop (nhds 1)
 150  correction_to_zero : Filter.Tendsto (fun N : ℝ => correction_RS N)
 151                        Filter.atTop (nhds 0)
 152  gap_to_zero : Filter.Tendsto (fun N : ℝ => C_RS N - C_classical N)
 153                 Filter.atTop (nhds 0)
 154  strict_pos_at_finite_N : ∀ {N : ℝ}, 0 < N → 0 < correction_RS N
 155  strict_anti_in_N : ∀ {N₁ N₂ : ℝ}, 0 < N₁ → N₁ < N₂ →
 156    correction_RS N₂ < correction_RS N₁
 157
 158def shannonHighNLimitCert : ShannonHighNLimitCert where
 159  inner_to_one := inner_arg_tendsto_one
 160  correction_to_zero := correction_RS_tendsto_zero
 161  gap_to_zero := C_RS_minus_C_classical_tendsto_zero
 162  strict_pos_at_finite_N := @correction_RS_strictly_pos
 163  strict_anti_in_N := @correction_RS_strict_anti
 164
 165/-! ## §5. One-statement summary -/
 166
 167/-- **SHANNON HIGH-N LIMIT ONE-STATEMENT.** Three structural facts:
 168
 169(1) The RS correction `correction_RS(N) = log₂(1 + 1/(φ·N))` is
 170    strictly positive at any finite N > 0.
 171(2) The correction is monotone decreasing in N (more bits ⇒ less
 172    correction).
 173(3) The correction tends to 0 as N → ∞, recovering classical Shannon
 174    `C(N) = log₂ N` exactly. -/
 175theorem shannon_high_N_limit_one_statement :
 176    (∀ {N : ℝ}, 0 < N → 0 < correction_RS N) ∧
 177    (∀ {N₁ N₂ : ℝ}, 0 < N₁ → N₁ < N₂ → correction_RS N₂ < correction_RS N₁) ∧
 178    Filter.Tendsto (fun N : ℝ => correction_RS N) Filter.atTop (nhds 0) :=
 179  ⟨@correction_RS_strictly_pos, @correction_RS_strict_anti,
 180   correction_RS_tendsto_zero⟩
 181
 182end
 183
 184end ShannonHighNLimit
 185end Information
 186end IndisputableMonolith
 187