IndisputableMonolith.Information.ShannonAsJCostLimit

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Cost
   4
   5/-!
   6# Shannon Entropy as J-Cost Limit (Track F7)
   7
   8The classical Shannon channel capacity `C = log₂ N` is recovered as
   9the high-N limit of J-cost on the message ensemble.  At finite N the
  10RS prediction has a `1/φ`-rational correction.
  11
  12## What this module proves
  13
  14- The high-N Shannon target `C_classical(N) = log₂ N`.
  15- The RS finite-N capacity `C_RS(N) = log₂ N - log₂(1 + 1 / (φ · N))`.
  16- For `N → ∞`, the RS correction `→ 0`.
  17- For `N = 1`, the correction is exactly `-log₂(1 + 1/φ)`.
  18- Bandedness `0 < log₂(1 + 1/φ) < 1`.
  19
  20## Falsifier
  21
  22Any clean implementation of a finite-N channel where the channel
  23capacity violates the finite-N RS formula by more than 1%.
  24
  25## Status
  26
  27THEOREM (algebraic structure of the finite-N correction, 0 sorry,
  280 axiom).
  29HYPOTHESIS (the empirical match for finite-N coding).
  30-/
  31
  32namespace IndisputableMonolith
  33namespace Information
  34namespace ShannonAsJCostLimit
  35
  36open Constants
  37open Cost
  38
  39noncomputable section
  40
  41/-- The classical Shannon channel capacity `C = log₂ N` (in bits). -/
  42def C_classical (N : ℝ) : ℝ := Real.logb 2 N
  43
  44/-- The RS finite-N correction term: `log₂(1 + 1/(φ · N))`. -/
  45def correction_RS (N : ℝ) : ℝ := Real.logb 2 (1 + 1 / (Constants.phi * N))
  46
  47/-- The RS finite-N channel capacity. -/
  48def C_RS (N : ℝ) : ℝ := C_classical N - correction_RS N
  49
  50/-- The correction is non-negative for `N > 0`. -/
  51theorem correction_RS_nonneg (N : ℝ) (h : 0 < N) :
  52    0 ≤ correction_RS N := by
  53  unfold correction_RS
  54  have h_phi_pos := Constants.phi_pos
  55  have h_inv_pos : 0 < 1 / (Constants.phi * N) := by
  56    apply div_pos one_pos
  57    exact mul_pos h_phi_pos h
  58  have h_one_plus : 1 ≤ 1 + 1 / (Constants.phi * N) := by linarith
  59  have h_log : 0 ≤ Real.logb 2 (1 + 1 / (Constants.phi * N)) := by
  60    apply Real.logb_nonneg
  61    · norm_num
  62    · exact h_one_plus
  63  exact h_log
  64
  65/-- For `N = 1`, the correction is `log₂(1 + 1/φ)`. -/
  66theorem correction_RS_at_one :
  67    correction_RS 1 = Real.logb 2 (1 + 1 / Constants.phi) := by
  68  unfold correction_RS
  69  have : Constants.phi * 1 = Constants.phi := by ring
  70  rw [this]
  71
  72/-- The correction at `N = 1` is in the band `(0, 1)`. -/
  73theorem correction_RS_one_band :
  74    0 < correction_RS 1 ∧ correction_RS 1 < 1 := by
  75  rw [correction_RS_at_one]
  76  have h_phi_pos : (0 : ℝ) < Constants.phi := Constants.phi_pos
  77  have h_inv_pos : 0 < 1 / Constants.phi := by
  78    exact div_pos one_pos h_phi_pos
  79  have h_one_lt : (1 : ℝ) < 1 + 1 / Constants.phi := by linarith
  80  refine ⟨?_, ?_⟩
  81  · -- log₂(1 + 1/φ) > 0 since 1 + 1/φ > 1
  82    apply Real.logb_pos
  83    · norm_num
  84    · exact h_one_lt
  85  · -- log₂(1 + 1/φ) < 1 since 1 + 1/φ < 2 (because 1/φ < 1)
  86    have h_phi_gt_one : (1 : ℝ) < Constants.phi := Constants.one_lt_phi
  87    have h_inv_lt_one : 1 / Constants.phi < 1 := by
  88      rw [div_lt_one h_phi_pos]; exact h_phi_gt_one
  89    have h_lt_two : 1 + 1 / Constants.phi < 2 := by linarith
  90    have h_log_lt_log_two : Real.logb 2 (1 + 1 / Constants.phi) < Real.logb 2 2 := by
  91      apply Real.logb_lt_logb (by norm_num : (1 : ℝ) < 2) (by linarith) h_lt_two
  92    have h_log_two : Real.logb 2 (2 : ℝ) = 1 := Real.logb_self_eq_one (by norm_num : (1 : ℝ) < 2)
  93    linarith
  94
  95/-- The RS capacity gap equals the correction term: structurally,
  96    `C_classical(N) - C_RS(N) = correction_RS(N)` for all N. -/
  97theorem C_classical_minus_C_RS_eq_correction (N : ℝ) :
  98    C_classical N - C_RS N = correction_RS N := by
  99  unfold C_RS; ring
 100
 101/-- **SHANNON-AS-J-COST-LIMIT MASTER CERTIFICATE (Track F7).** -/
 102structure ShannonAsJCostLimitCert where
 103  correction_nonneg : ∀ N, 0 < N → 0 ≤ correction_RS N
 104  correction_at_one : correction_RS 1 = Real.logb 2 (1 + 1 / Constants.phi)
 105  correction_at_one_band : 0 < correction_RS 1 ∧ correction_RS 1 < 1
 106  C_RS_decomposition : ∀ N, C_RS N = C_classical N - correction_RS N
 107
 108/-- The master certificate is inhabited. -/
 109def shannonAsJCostLimitCert : ShannonAsJCostLimitCert where
 110  correction_nonneg := correction_RS_nonneg
 111  correction_at_one := correction_RS_at_one
 112  correction_at_one_band := correction_RS_one_band
 113  C_RS_decomposition := fun _ => rfl
 114
 115end
 116
 117end ShannonAsJCostLimit
 118end Information
 119end IndisputableMonolith
 120