Information Shannon As Jcost Limit Correction Rs Nonneg

The finite-N correction

Claude Shannon's 1948 channel capacity, the maximum rate at which information can be sent reliably over a noisy channel, is usually written as C = log₂ N, where N is the number of possible messages. For a very large N, this classical formula is an excellent approximation. The Recognition Science framework, which models physical structure from a discrete record of recognition events, examines what happens when N is not large. Its library of machine-checked formal theorems defines a finite-N capacity, C_RS(N), that subtracts a correction term from the classical value.

That correction term is the subject of the theorem correction_RS_nonneg. It states that for any positive number of messages N, the correction, defined as log₂(1 + 1/(φ·N)), is greater than or equal to zero. Here φ is the golden ratio. The proof is a formal theorem in the framework's library, checked with no gaps and no special axioms. The theorem's content is plain: the finite-N capacity never exceeds the classical Shannon capacity. The correction is a penalty, not a bonus, for working with a small message set.

The framework also proves the correction is bounded. For N = 1, the correction is exactly log₂(1 + 1/φ), a value that lies strictly between 0 and 1. As N grows, the correction shrinks toward zero, so the classical capacity C = log₂ N is recovered in the high-N limit. The framework labels the algebraic structure of this correction a theorem, but it labels the empirical match for finite-N coding a hypothesis. A named falsifier exists: any clean implementation of a finite-N channel whose capacity violates the finite-N formula by more than 1 percent would refute that hypothesis.

In Recognition Science, this correction is a consequence of the framework's forced cost function, not an independent postulate. The framework's account is that the cost of recognition, which must equal J(x) = (x + 1/x)/2 - 1, leads to this specific rational correction involving φ. The classical Shannon result is not contradicted; it is derived as a limit. The framework's contribution is to sharpen the classical formula for finite N, and to prove that the sharpening is always a subtraction, never an addition.

/-- The correction is non-negative for `N > 0`. -/
theorem correction_RS_nonneg (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_plus : 1 ≤ 1 + 1 / (Constants.phi * N) := by linarith
  have h_log : 0 ≤ Real.logb 2 (1 + 1 / (Constants.phi * N)) := by
    apply Real.logb_nonneg
    · norm_num
    · exact h_one_plus
  exact h_log

/-- For `N = 1`, the correction is `log₂(1 + 1/φ)`. -/
theorem correction_RS_at_one :
    correction_RS 1 = Real.logb 2 (1 + 1 / Constants.phi) := by
  unfold correction_RS
  have : Constants.phi * 1 = Constants.phi := by ring
  rw [this]

/-- The correction at `N = 1` is in the band `(0, 1)`. -/
theorem correction_RS_one_band :
    0 < correction_RS 1 ∧ correction_RS 1 < 1 := by
  rw [correction_RS_at_one]
  have h_phi_pos : (0 : ℝ) < Constants.phi := Constants.phi_pos
  have h_inv_pos : 0 < 1 / Constants.phi := by
    exact div_pos one_pos h_phi_pos
  have h_one_lt : (1 : ℝ) < 1 + 1 / Constants.phi := by linarith
  refine ⟨?_, ?_⟩
  · -- log₂(1 + 1/φ) > 0 since 1 + 1/φ > 1
    apply Real.logb_pos
    · norm_num
    · exact h_one_lt
  · -- log₂(1 + 1/φ) < 1 since 1 + 1/φ < 2 (because 1/φ < 1)
    have h_phi_gt_one : (1 : ℝ) < Constants.phi := Constants.one_lt_phi
    have h_inv_lt_one : 1 / Constants.phi < 1 := by
      rw [div_lt_one h_phi_pos]; exact h_phi_gt_one
    have h_lt_two : 1 + 1 / Constants.phi < 2 := by linarith
    have h_log_lt_log_two : Real.logb 2 (1 + 1 / Constants.phi) < Real.logb 2 2 := by
      apply Real.logb_lt_logb (by norm_num : (1 : ℝ) < 2) (by linarith) h_lt_two
    have h_log_two : Real.logb 2 (2 : ℝ) = 1 := Real.logb_self_eq_one (by norm_num : (1 : ℝ) < 2)
    linarith

/-- The RS capacity gap equals the correction term: structurally,
    `C_classical(N) - C_RS(N) = correction_RS(N)` for all N. -/
theorem C_classical_minus_C_RS_eq_correction (N : ℝ) :
    C_classical N - C_RS N = correction_RS N := by
  unfold C_RS; ring

/-- The master certificate is inhabited. -/
def shannonAsJCostLimitCert : ShannonAsJCostLimitCert where
  correction_nonneg := correction_RS_nonneg
  correction_at_one := correction_RS_at_one
  correction_at_one_band := correction_RS_one_band
  C_RS_decomposition := fun _ => rfl

What this page does not claim

This theorem does not claim the empirical validity of the finite-N correction; that remains a hypothesis. This theorem does not claim to derive Shannon's capacity from Recognition Science; it only recovers it as a limit. This theorem does not claim the correction is the only possible finite-N correction, only that this specific one is non-negative.

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/ShannonAsJCostLimit.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: