Encyclopedia Information Information Shannon High Nlimit Correction Rs Tendsto Zero

ARTICLE 4 claims 4 theorems

Information Shannon High Nlimit Correction Rs Tendsto Zero

A small correction term in a formula for information capacity vanishes as the number of symbols grows, recovering the classical Shannon result exactly.

Verify this page

The finite-N correction

In information theory, Shannon's capacity formula C(N) = log₂ N gives the maximum rate at which data can be sent reliably through a noiseless channel using N distinct symbols. For a finite alphabet, however, a real system may need a correction term to account for the cost of distinguishing symbols. The Recognition Science framework models this by adding a finite-size correction to the classical formula: C_RS(N) = log₂ N − log₂(1 + 1/(φ·N)), where φ is the golden ratio, about 1.618. The correction term, correction_RS(N) = log₂(1 + 1/(φ·N)), is strictly positive for any finite N > 0, meaning the RS capacity is always slightly below the classical value at finite N.

The key result, proved in the framework's machine-checked library of formal theorems, is that this correction vanishes as N grows without bound. Formally, correction_RS(N) tends to 0 as N → ∞, and consequently the RS capacity C_RS(N) minus the classical capacity C_classical(N) also tends to 0. In plain terms: for a large enough alphabet, the RS formula becomes indistinguishable from Shannon's original C(N) = log₂ N. The correction is also monotone decreasing in N: more symbols means a smaller correction, and the gap between the two formulas shrinks steadily.

The theorem does not claim that the correction is zero at any finite N; it is strictly positive for every finite N, only approaching zero in the limit. It does not claim that the RS formula is more accurate than the classical one at any particular N; the theorem only establishes the limit and the monotonicity, not an empirical advantage. It also does not claim that the golden ratio φ itself is derived from information theory here; φ enters as a constant from the framework's own structure, not as a consequence of this theorem.

THEOREM correction_RS_strictly_pos · IndisputableMonolith/Information/ShannonHighNLimit.lean
correction_RS_strictly_pos · IndisputableMonolith/Information/ShannonHighNLimit.lean:104 
/-- **THEOREM.** For any finite `N > 0`, the correction is strictly positive. -/
theorem correction_RS_strictly_pos {N : ℝ} (h : 0 < N) :
    0 < correction_RS N := by
  unfold correction_RS
  have h_phi_pos := Constants.phi_pos
  have h_inv_pos : 0 < 1 / (Constants.phi * N) := by
    apply div_pos one_pos
    exact mul_pos h_phi_pos h
  have h_one_lt : (1 : ℝ) < 1 + 1 / (Constants.phi * N) := by linarith
  exact Real.logb_pos (by norm_num : (1 : ℝ) < 2) h_one_lt
THEOREM correction_RS_tendsto_zero · IndisputableMonolith/Information/ShannonHighNLimit.lean
correction_RS_tendsto_zero · IndisputableMonolith/Information/ShannonHighNLimit.lean:69 
/-- **THEOREM.** The RS correction tends to 0 as `N → ∞`. -/
theorem correction_RS_tendsto_zero :
    Filter.Tendsto (fun N : ℝ => correction_RS N) Filter.atTop (nhds 0) := by
  -- correction_RS N = log₂(1 + 1/(φ·N)); inner arg → 1; log₂ 1 = 0.
  unfold correction_RS
  have h_inner := inner_arg_tendsto_one
  -- Use Real.continuousAt_logb at 1.
  have h_logb_cont_at_one : Filter.Tendsto (Real.logb 2)
      (nhds 1) (nhds (Real.logb 2 1)) := by
    have h_one_ne : (1 : ℝ) ≠ 0 := one_ne_zero
    exact (Real.continuousAt_logb h_one_ne).tendsto
  have h_log : Filter.Tendsto
      (fun N : ℝ => Real.logb 2 (1 + 1 / (Constants.phi * N)))
      Filter.atTop (nhds (Real.logb 2 1)) :=
    h_logb_cont_at_one.comp h_inner
  rw [show Real.logb 2 (1 : ℝ) = 0 from Real.logb_one] at h_log
  exact h_log
THEOREM C_RS_minus_C_classical_tendsto_zero · IndisputableMonolith/Information/ShannonHighNLimit.lean
C_RS_minus_C_classical_tendsto_zero · IndisputableMonolith/Information/ShannonHighNLimit.lean:87 
/-- **THEOREM.** Classical Shannon capacity is the high-N limit of `C_RS`:
`C_RS(N) - C_classical(N) → 0` as `N → ∞`. -/
theorem C_RS_minus_C_classical_tendsto_zero :
    Filter.Tendsto (fun N : ℝ => C_RS N - C_classical N) Filter.atTop (nhds 0) := by
  have h_corr_tendsto := correction_RS_tendsto_zero
  -- C_RS - C_classical = -correction_RS, which tends to -0 = 0.
  have h_eq : (fun N : ℝ => C_RS N - C_classical N) = (fun N : ℝ => -(correction_RS N)) := by
    funext N
    unfold C_RS
    ring
  rw [h_eq]
  have h_neg := h_corr_tendsto.neg
  simp at h_neg
  exact h_neg
THEOREM correction_RS_strict_anti · IndisputableMonolith/Information/ShannonHighNLimit.lean
correction_RS_strict_anti · IndisputableMonolith/Information/ShannonHighNLimit.lean:117 
/-- **THEOREM.** The correction is monotone decreasing in N. -/
theorem correction_RS_strict_anti {N₁ N₂ : ℝ} (h_pos : 0 < N₁) (h_lt : N₁ < N₂) :
    correction_RS N₂ < correction_RS N₁ := by
  unfold correction_RS
  have h_phi_pos := Constants.phi_pos
  -- 1/(φ·N₂) < 1/(φ·N₁), since N₁ < N₂ and φ > 0.
  have h_pos₂ : 0 < N₂ := lt_trans h_pos h_lt
  have h_phiN₁_pos : 0 < Constants.phi * N₁ := mul_pos h_phi_pos h_pos
  have h_phiN₂_pos : 0 < Constants.phi * N₂ := mul_pos h_phi_pos h_pos₂
  have h_phiN_lt : Constants.phi * N₁ < Constants.phi * N₂ :=
    mul_lt_mul_of_pos_left h_lt h_phi_pos
  have h_inv : 1 / (Constants.phi * N₂) < 1 / (Constants.phi * N₁) := by
    apply div_lt_div_of_pos_left one_pos h_phiN₁_pos h_phiN_lt
  have h_arg_lt : 1 + 1 / (Constants.phi * N₂) < 1 + 1 / (Constants.phi * N₁) := by
    linarith
  have h_arg₂_pos : 0 < 1 + 1 / (Constants.phi * N₂) := by
    have : 0 < 1 / (Constants.phi * N₂) := div_pos one_pos h_phiN₂_pos
    linarith
  exact Real.logb_lt_logb (by norm_num : (1 : ℝ) < 2) h_arg₂_pos h_arg_lt

What this page does not claim

The correction is never zero at any finite N; it only approaches zero in the limit. The RS formula is more accurate than the classical Shannon formula at any finite N. The golden ratio φ is derived from information theory by this theorem; it is a constant from the framework.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/ShannonHighNLimit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND