Information Shannon High Nlimit Inner Arg Tendsto One

The vanishing correction

Claude Shannon's 1948 formula for the capacity of a noiseless channel with N symbols is C(N) = log2(N), the base-2 logarithm of the number of symbols. The formula answers a practical question: with N distinct signals, how many bits of information can each one carry? The answer grows without bound as N grows, but it grows slowly, and the formula is exact for any N.

In Recognition Science, the framework models the same capacity with an extra term. Its finite-N capacity is C_RS(N) = log2(1 + 1/(φ·N)), where φ is the golden ratio, about 1.618. The extra term inside the logarithm is the framework's correction to Shannon's classical value. The central theorem, named inner_arg_tendsto_one, proves that this inner argument, 1 + 1/(φ·N), tends to 1 as N tends to infinity. Since log2(1) = 0, the correction term itself tends to 0, and the framework's capacity C_RS(N) converges to the classical Shannon capacity C(N) = log2(N). The machine-checked library of formal theorems verifies this limit, along with the stronger claim that the difference C_RS(N) - C_classical(N) tends to 0.

The theorem also establishes two structural facts about the correction at finite N. For any finite positive N, the correction is strictly positive, meaning the framework's capacity is always slightly larger than the classical value. And the correction decreases monotonically as N grows: more symbols mean a smaller adjustment. The correction is largest at N = 1, where the inner argument is 1 + 1/φ, and it shrinks steadily toward zero.

In Recognition Science, this result is part of a chain that derives physical constants from a forced cost function. The golden ratio appears in the correction because the framework's constants, including φ, are not free parameters but consequences of the forcing chain. The limit theorem shows that the framework's departure from classical information theory is a finite-size effect that vanishes in the large-alphabet limit, not a permanent alternative to Shannon's formula.

What the theorem does not claim is just as important as what it proves. It does not prove that the correction formula is physically realized in any real communication system. It does not claim that the golden ratio is a fundamental constant of information theory. It only establishes the mathematical limit behavior of a specific definition within the framework. The theorem is a statement about the framework's own model, not an empirical measurement of any actual channel.

/-- **THEOREM.** As N → ∞, the inner argument `1 + 1/(φ·N) → 1`. -/
theorem inner_arg_tendsto_one :
    Filter.Tendsto (fun N : ℝ => 1 + 1 / (Constants.phi * N))
      Filter.atTop (nhds 1) := by
  have h_phi_pos := Constants.phi_pos
  -- φ·N → ∞, so (φ·N)⁻¹ → 0.
  have h_mul : Filter.Tendsto (fun N : ℝ => Constants.phi * N)
      Filter.atTop Filter.atTop :=
    Filter.Tendsto.const_mul_atTop h_phi_pos Filter.tendsto_id
  have h_inv := Filter.Tendsto.inv_tendsto_atTop h_mul
  -- Convert (φ·N)⁻¹ to 1/(φ·N).
  have h_one_div : Filter.Tendsto (fun N : ℝ => 1 / (Constants.phi * N))
      Filter.atTop (nhds 0) := by
    have h_eq : (fun N : ℝ => 1 / (Constants.phi * N))
        = (fun N : ℝ => (Constants.phi * N)⁻¹) := by
      funext N; rw [one_div]
    rw [h_eq]
    exact h_inv
  -- 1 + 1/(φ·N) → 1 + 0 = 1.
  have h_sum := (tendsto_const_nhds (x := (1 : ℝ))).add h_one_div
  rw [show (1 : ℝ) + 0 = 1 from by ring] at h_sum
  exact h_sum

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

What this page does not claim

The theorem does not prove the correction formula describes any real communication system. It does not claim the golden ratio is a fundamental constant of information theory. It does not establish the framework's capacity model as empirically valid at finite N.

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: