Information Shannon High Nlimit Correction Rs Strictly Pos

The finite-N correction

Claude Shannon's channel capacity formula, C(N) = log₂ N, describes the maximum rate at which information can be sent reliably through a noiseless channel using an alphabet of N symbols. The formula is a limit: it holds exactly when N is infinite. For any finite alphabet, the true capacity is slightly lower than log₂ N. The Recognition Science framework, a system that derives physical and mathematical structure from a forced cost of recognition, models this finite-size gap with a specific correction term.

Within the framework, the correction is defined as correction_RS(N) = log₂(1 + 1/(φ·N)), where φ is the golden ratio, approximately 1.618. The framework's machine-checked library of formal theorems proves that this correction is strictly positive for any finite N greater than zero. In plain language: for any finite alphabet, the true capacity is always a little less than the classical Shannon limit, never more. The gap is real and it shrinks as N grows.

The same library proves the correction is monotone decreasing in N: larger alphabets suffer smaller corrections. As N tends to infinity, the correction tends to zero, and the framework's capacity C_RS(N) recovers the classical Shannon capacity C(N) = log₂ N exactly. The framework does not claim the correction is large, only that it is positive at every finite N and vanishes in the limit.

The framework's proof of strict positivity is a theorem in its formal library, not a hypothesis or a model choice. The declaration correction_RS_strictly_pos states: for any real N with 0 < N, the correction is greater than zero. This is a precise, machine-checked statement about the framework's own definition of capacity. It does not assert that the framework's correction matches any real-world measurement of channel capacity, nor that the golden ratio appears in Shannon's original work.

In Recognition Science, this result is one step in a larger chain that derives constants like the golden ratio from the forced cost of recognition. For a reader, the practical takeaway is simple: the framework's finite-N correction is a small, positive, shrinking quantity, and the classical Shannon formula is its infinite-N limit. The framework does not claim this correction is the only possible finite-size correction, nor that it has been verified against experimental data.

/-- **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.** 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.** 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.** 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

The correction has been verified against experimental channel capacity measurements. The golden ratio appears in Shannon's original information theory. The framework's capacity formula is the only possible finite-size correction to Shannon's limit.

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: