Encyclopedia Information Information Shannon High Nlimit Shannon High N Limit One Statement
ARTICLE 4 claims 4 theorems
Information Shannon High Nlimit Shannon High N Limit One Statement
Shannon's classic formula for information capacity is what remains when a finite-size correction, derived from recognition costs, shrinks to nothing.
The high-N limit
Claude Shannon's 1948 formula, C(N) = log₂ N, gives the maximum number of bits that can be transmitted per symbol over a noiseless channel with N distinct symbols. The formula is exact for an ideal, infinitely precise system. Real systems have finite resources, and the Recognition Science framework asks what happens to Shannon's clean result when those resources are accounted for.
Within the framework, a finite system of N symbols carries a small correction to Shannon's formula. The framework models this correction as log₂(1 + 1/(φ·N)), where φ is the golden ratio, about 1.618. This correction is strictly positive for any finite N: a real system with finite resources always carries slightly less information than the ideal formula suggests. The correction is also monotone decreasing; as N grows, the penalty shrinks.
The central theorem, named shannon_high_N_limit_one_statement, bundles these facts into one statement. It proves that the correction is positive at every finite N, that it decreases as N increases, and that it tends to zero as N goes to infinity. The last fact is the punchline: in the limit of infinitely many symbols, the framework's corrected capacity C_RS(N) converges exactly to Shannon's classical C(N) = log₂ N.
In Recognition Science, this is the high-N limit. The framework's finite-size correction vanishes, and the classical formula is recovered exactly. The theorem does not say that the correction is zero at any finite N, nor does it say how quickly the correction vanishes. It also does not claim that the golden ratio φ is derived from Shannon's work; φ enters from the framework's own cost function, not from information theory.
THEOREM correction_RS_strictly_pos · IndisputableMonolith/Information/ShannonHighNLimit.lean
/-- **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 correction_RS_strict_anti · IndisputableMonolith/Information/ShannonHighNLimit.lean
/-- **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 shannon_high_N_limit_one_statement · IndisputableMonolith/Information/ShannonHighNLimit.lean
/-- **SHANNON HIGH-N LIMIT ONE-STATEMENT.** Three structural facts:
(1) The RS correction `correction_RS(N) = log₂(1 + 1/(φ·N))` is
strictly positive at any finite N > 0.
(2) The correction is monotone decreasing in N (more bits ⇒ less
correction).
(3) The correction tends to 0 as N → ∞, recovering classical Shannon
`C(N) = log₂ N` exactly. -/
theorem shannon_high_N_limit_one_statement :
(∀ {N : ℝ}, 0 < N → 0 < correction_RS N) ∧
(∀ {N₁ N₂ : ℝ}, 0 < N₁ → N₁ < N₂ → correction_RS N₂ < correction_RS N₁) ∧
Filter.Tendsto (fun N : ℝ => correction_RS N) Filter.atTop (nhds 0) :=
⟨@correction_RS_strictly_pos, @correction_RS_strict_anti,
correction_RS_tendsto_zero⟩
THEOREM C_RS_minus_C_classical_tendsto_zero · IndisputableMonolith/Information/ShannonHighNLimit.lean
/-- **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 theorem does not claim the correction is zero at any finite N, only that it tends to zero. The theorem does not state the rate at which the correction vanishes, only that it vanishes. The golden ratio φ is not derived from Shannon's work; it enters from the framework's own cost function.
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:
- What is the derivation of the correction log₂(1 + 1/(φ·N)) from the framework's cost function?
- At what finite N does the correction become negligible compared to the measurement error of a real channel?
- Does the framework's correction apply to noisy channels, or only to the noiseless case Shannon's formula describes?
- What is the empirical status of the correction: has any experiment measured a deviation from Shannon's formula that matches this shape?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
THEOREM correction_RS_strictly_pos · IndisputableMonolith/Information/ShannonHighNLimit.lean
/-- **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_ltThe correction is strictly positive for any finite N: a real system with finite resources always carries slightly less information than the ideal formula suggests. correction_RS_strictly_pos · IndisputableMonolith/Information/ShannonHighNLimit.leanTHEOREM correction_RS_strict_anti · IndisputableMonolith/Information/ShannonHighNLimit.lean
/-- **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_ltThe correction is also monotone decreasing; as N grows, the penalty shrinks. correction_RS_strict_anti · IndisputableMonolith/Information/ShannonHighNLimit.leanTHEOREM shannon_high_N_limit_one_statement · IndisputableMonolith/Information/ShannonHighNLimit.lean
/-- **SHANNON HIGH-N LIMIT ONE-STATEMENT.** Three structural facts: (1) The RS correction `correction_RS(N) = log₂(1 + 1/(φ·N))` is strictly positive at any finite N > 0. (2) The correction is monotone decreasing in N (more bits ⇒ less correction). (3) The correction tends to 0 as N → ∞, recovering classical Shannon `C(N) = log₂ N` exactly. -/ theorem shannon_high_N_limit_one_statement : (∀ {N : ℝ}, 0 < N → 0 < correction_RS N) ∧ (∀ {N₁ N₂ : ℝ}, 0 < N₁ → N₁ < N₂ → correction_RS N₂ < correction_RS N₁) ∧ Filter.Tendsto (fun N : ℝ => correction_RS N) Filter.atTop (nhds 0) := ⟨@correction_RS_strictly_pos, @correction_RS_strict_anti, correction_RS_tendsto_zero⟩It proves that the correction is positive at every finite N, that it decreases as N increases, and that it tends to zero as N goes to infinity. shannon_high_N_limit_one_statement · IndisputableMonolith/Information/ShannonHighNLimit.leanTHEOREM C_RS_minus_C_classical_tendsto_zero · IndisputableMonolith/Information/ShannonHighNLimit.lean
/-- **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_negin the limit of infinitely many symbols, the framework's corrected capacity C_RS(N) converges exactly to Shannon's classical C(N) = log₂ N. C_RS_minus_C_classical_tendsto_zero · IndisputableMonolith/Information/ShannonHighNLimit.lean