Information Shannon High Nlimit Correction Rs Strict Anti

The shrinking correction

In information theory, Claude Shannon's channel capacity C(N) = log₂ N measures how many bits a noiseless channel can carry when it has N distinct symbols. The Recognition Science framework adds a small correction to this classical formula. The correction is defined as log₂(1 + 1/(φ·N)), where φ is the golden ratio, about 1.618. At any finite N greater than zero, this correction is strictly positive: the framework's capacity C_RS(N) is always slightly larger than the classical value.

The declaration correction_RS_strict_anti proves that this correction strictly decreases as N grows. If N₁ is a positive number and N₂ is any larger number, then the correction at N₂ is strictly smaller than the correction at N₁. In plain terms: the more symbols a channel has, the smaller the framework's adjustment becomes. The theorem is machine-checked in the framework's library of formal theorems, meaning the proof has been verified step by step by a computer.

This monotone decrease pairs with a companion result: as N tends to infinity, the correction tends to zero. Together the two facts mean the framework's capacity C_RS(N) converges to the classical Shannon capacity exactly in the high-N limit. The framework does not replace Shannon's formula; it adds a finite-size adjustment that fades away as the message space grows. The strict anti-monotonicity is the precise statement that the adjustment never reverses direction as N increases.

In Recognition Science, the correction reflects a forced cost of recognition at finite scales, a discrete record of events that classical information theory does not account for. The golden ratio enters because it is the unique self-similar scaling forced by the framework's cost function. But the theorem itself is narrow: it concerns only the behavior of one correction term as a real variable N grows. It does not say anything about how the correction behaves at finite N in absolute terms, only that it is positive and decreasing.

The practical consequence is a clear boundary between the framework's claim and classical theory. For any finite N, the framework predicts a measurable excess over Shannon's capacity. As N grows, that excess becomes negligible, and the classical formula is recovered exactly. The falsifier for the whole correction family is a coding experiment where the measured gap between classical and framework capacity deviates from log₂(1 + 1/(φ·N)) by more than one percent across N values from 1 to 64.

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

What this page does not claim

The theorem does not claim the correction is small in absolute terms at any specific finite N. The theorem does not claim the framework's capacity is achievable by any known coding scheme. The theorem does not claim the golden ratio is the only possible scaling for the correction.

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: