Information Shannon High Nlimit C Rs Minus C Classical Tendsto Zero

The high-N limit

Claude Shannon's 1948 formula for the capacity of a noiseless channel, C(N) = log₂ N, gives the maximum number of bits that can be transmitted per symbol when there are N possible symbols. It is one of the founding results of information theory. In the Recognition Science framework, a different derivation of capacity starts from a ledger, a discrete record of recognition events, and produces a finite-size correction to Shannon's formula. The central theorem in question, C_RS_minus_C_classical_tendsto_zero, proves that this correction vanishes as N grows without bound, so the Recognition Science capacity C_RS(N) converges to the classical value C(N) = log₂ N.

The proof is direct. The framework defines its capacity as C_RS(N) = log₂(1 + 1/(φ·N)), where φ is the golden ratio, approximately 1.618. The difference between the two capacities is therefore C_RS(N) - C(N) = -log₂(1 + 1/(φ·N)). As N tends to infinity, the term 1/(φ·N) tends to zero, so the logarithm tends to zero, and the difference tends to zero. The theorem establishes this limit formally: for any positive error bound, there exists a sufficiently large N such that the absolute difference is smaller than that bound. The proof is checked by a machine-checked library of formal theorems, meaning the logical steps are verified by a computer program.

The theorem also establishes two supporting facts about the correction. First, at any finite N greater than zero, the correction is strictly positive: the Recognition Science capacity is always slightly less than the classical capacity. Second, the correction decreases monotonically as N increases: adding more possible symbols shrinks the gap. These properties are proved for all real N greater than zero, not just for integer values, and they hold for every such N without exception.

In Recognition Science, this result is part of a larger program that derives physical and mathematical structure from the forced cost of recognition. The specific claim here is narrow and precise: the high-N limit of the Recognition Science capacity recovers the classical Shannon formula exactly. The theorem does not assert that the Recognition Science correction is the correct description of any real communication system at finite N. That is an empirical question, and the framework's own falsifier names a concrete test: a coding experiment at N values 1, 2, 4, 8, 16, 32, and 64 where the measured capacity differs from C_classical(N) by more than one percent from the predicted correction would refute the model.

What the theorem changes is the relationship between the two frameworks. It shows that the Recognition Science model is not a competitor to Shannon's formula in the large-N regime; it is a refinement that reduces to the classical result. The correction is a finite-size effect, like a boundary term in a physical theory that disappears in the thermodynamic limit. For a reader familiar with Shannon's work, the practical takeaway is that the Recognition Science capacity is a one-parameter family of curves that all converge to the same classical line, with the golden ratio setting the rate of approach.

/-- **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 claim that the Recognition Science capacity formula is the correct description of any real communication system at finite N. The theorem does not derive the golden ratio from information-theoretic first principles; it takes the constant as given from the framework's cost function. The theorem does not provide a constructive method for achieving the predicted capacity 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: