Encyclopedia Information Information Shannon High Nlimit

ARTICLE 5 claims 4 theorems 1 model

Information Shannon High Nlimit

Shannon's formula for channel capacity is the large-alphabet limit of a finite correction, and the framework proves the two converge.

Verify this page

The high-N limit

In information theory, Claude Shannon's capacity formula C(N) = log₂ N gives the maximum rate, in bits per symbol, at which information can be sent reliably over a channel with N distinct symbols. The formula is exact for an alphabet of size N, and it grows without bound as N increases. The Recognition Science framework starts from a different picture: it treats information as a recognition event, a discrete act of identifying one symbol among N, and asks what capacity looks like when the cost of that act is forced by the framework's own axioms.

That framework-derived capacity, written C_RS(N), differs from Shannon's classical value by a small correction: correction_RS(N) = log₂(1 + 1/(φ·N)), where φ is the golden ratio. The correction is strictly positive for any finite N, meaning the framework's capacity is always slightly less than the classical value. But the gap is not a contradiction; it is a finite-size effect. The module ShannonHighNLimit.lean proves, as a machine-checked theorem, that this correction tends to 0 as N tends to infinity. In the limit of infinitely many symbols, C_RS(N) and C_classical(N) become exactly equal.

The proof rests on three structural facts, each established in the Lean library. First, the correction is strictly positive for every finite N greater than 0. Second, it is monotonically decreasing: larger alphabets have smaller corrections. Third, and decisively, the correction tends to 0 in the limit. The library packages these as a single certificate, ShannonHighNLimitCert, and a one-statement theorem that bundles all three properties. The argument is elementary: as N grows, the inner term 1 + 1/(φ·N) approaches 1, and the logarithm of something approaching 1 approaches 0.

What this establishes in plain language is that the framework's account of information does not replace Shannon's; it refines it at finite scales and agrees with it exactly at the classical limit. The framework models a small penalty for small alphabets, a penalty that vanishes as the alphabet grows. This is a consistency result: the Recognition Science picture, built from recognition events and forced costs, reproduces the standard information-theoretic answer in the regime where classical theory is defined.

MODEL 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 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_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
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

What this page does not claim

This module does not prove that Shannon's formula is wrong at finite N; it proves a specific correction that vanishes in the limit. The golden ratio φ in the correction is a constant from the framework, not a free parameter fitted to data. The theorem does not claim that the framework's capacity is the only possible finite-N refinement of Shannon's formula.

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