Information Shannon High Nlimit Shannon High Nlimit Cert

The high-N limit certificate

In information theory, Shannon's capacity formula C(N) = log₂ N describes the maximum rate at which data can be sent reliably using N distinct symbols. The Recognition Science framework, which models information through a discrete ledger (a record of recognition events), introduces a finite-size correction to this formula. The correction is written as log₂(1 + 1/(φ·N)), where φ is the golden ratio, approximately 1.618. This correction accounts for the cost of recognizing symbols when the set is small.

The declaration ShannonHighNLimitCert is a machine-checked certificate, a packaged collection of five formal theorems from the framework's library of verified mathematics. It establishes three structural facts about the correction. First, the correction is strictly positive for any finite N greater than zero, meaning the framework's capacity is always slightly below the classical value at finite sizes. Second, the correction decreases monotonically as N grows: more symbols mean a smaller correction. Third, and most importantly, the correction tends to zero as N approaches infinity. This last fact means that in the limit of infinitely many symbols, the Recognition Science capacity C_RS(N) converges exactly to the classical Shannon capacity C(N) = log₂ N.

The certificate bundles these results into a single object: it packages the proofs that the inner argument 1 + 1/(φ·N) tends to 1, the correction tends to 0, the gap between C_RS and C_classical tends to 0, the correction is strictly positive at finite N, and the correction is strictly decreasing. The existence of this certificate is itself a theorem, constructed from the individual proofs. The one-statement summary theorem condenses the three structural facts into a single conjunction, all verified in the framework's formal system.

What this certificate does not claim is equally important. It does not assert that the Recognition Science correction formula is the correct description of any physical or experimental system. The certificate is a purely mathematical result about the limit behavior of a defined function. The falsifier listed in the framework's documentation is a proposed finite-N coding experiment that would test whether the correction matches measured capacity to better than 1% across N ∈ {1, 2, 4, 8, 16, 32, 64}. That experiment has not been run, and the certificate makes no prediction about its outcome. The certificate also does not claim that the golden ratio φ is derived from information theory; φ enters as a constant in the definition of the correction, not as a consequence of the limit theorem.

/-- **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 certificate does not claim the correction formula is experimentally verified. The certificate does not claim the golden ratio is derived from information theory. The certificate does not claim the correction applies to any specific physical system.

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: