Information Quantum Channel Capacity From Phi Correction

The finite-N correction

In information theory, the capacity of a channel is the maximum rate at which data can be sent reliably. The classical formula, due to Claude Shannon in 1948, is C = log₂(1 + S/N), where S is signal power and N is noise power. Quantum versions of this capacity, which account for entanglement or coherent information, face a subtlety: when the input is sent in blocks of finite length, the ideal formula is only an approximation. The Recognition Science framework models a correction to this ideal, one that depends on the block length and shrinks as the block grows.

The correction is defined as 1 / (φ · N), where φ is the golden ratio, about 1.618, and N is the number of input symbols in a block. The framework's machine-checked library of formal theorems proves three properties of this correction. It is always positive for any positive N, so it never flips sign. It strictly decreases as N increases, meaning longer blocks get a smaller correction. And it is bounded above by 1/N, so it tends to zero as N grows large. These are the basic analytic facts one would want from any sensible finite-size correction.

In Recognition Science, this correction is not an arbitrary fudge factor. The golden ratio appears throughout the framework as a forced constant, derived from the cost function that governs recognition events. The correction factor is one more place where that constant shows up, here modulating the gap between ideal and finite-block capacity. The framework's library records this as a certificate: a bundled proof that the correction is positive, decreasing, and bounded by 1/N.

What the declaration does not claim is just as important. It does not claim that this correction has been measured in any experiment. It does not claim that the golden ratio is the only possible source of such a correction, or that the framework's derivation of φ is physically validated. The theorems prove the mathematical properties of the defined correction, nothing more. The physical relevance of the correction, whether real channels exhibit it, remains an open question.

/-- The φ-ladder finite-N correction factor for quantum channel
capacity at input-symbol-count `N`. -/
def correction (N : ℕ) (hN : 0 < N) : ℝ := 1 / (phi * (N : ℝ))

/-- Correction is strictly positive at every positive `N`. -/
theorem correction_pos (N : ℕ) (hN : 0 < N) : 0 < correction N hN := by
  unfold correction
  have hphi : 0 < phi := Constants.phi_pos
  have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
  positivity

/-- Correction strictly decreases with `N` (from `N` to `N+1`). -/
theorem correction_strictly_decreasing (N : ℕ) (hN : 0 < N) :
    correction (N + 1) (Nat.succ_pos _) < correction N hN := by
  unfold correction
  have hphi : 0 < phi := Constants.phi_pos
  have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
  have hN1pos : (0 : ℝ) < ((N + 1 : ℕ) : ℝ) := by exact_mod_cast Nat.succ_pos _
  have hphiN_pos : (0 : ℝ) < phi * (N : ℝ) := by positivity
  have hphiN1_pos : (0 : ℝ) < phi * ((N + 1 : ℕ) : ℝ) := by positivity
  have hphi_le_strict : phi * (N : ℝ) < phi * ((N + 1 : ℕ) : ℝ) := by
    apply mul_lt_mul_of_pos_left ?_ hphi
    exact_mod_cast Nat.lt_succ_self N
  exact one_div_lt_one_div_of_lt hphiN_pos hphi_le_strict

/-- Correction tends to 0 as `N → ∞` (statement form using single
positive `N`; the limit is the standard `1/N → 0`). -/
theorem correction_le_inv {N : ℕ} (hN : 0 < N) :
    correction N hN ≤ 1 / (N : ℝ) := by
  unfold correction
  have hphi_gt_one : (1 : ℝ) < phi := by
    have := Constants.phi_gt_onePointFive; linarith
  have hphi : 0 < phi := Constants.phi_pos
  have hNpos : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN
  have hphiN : 0 < phi * (N : ℝ) := by positivity
  have hN_le : (N : ℝ) ≤ phi * (N : ℝ) := by
    have : (1 : ℝ) * (N : ℝ) ≤ phi * (N : ℝ) :=
      mul_le_mul_of_nonneg_right (le_of_lt hphi_gt_one) (le_of_lt hNpos)
    simpa using this
  exact one_div_le_one_div_of_le hNpos hN_le

What this page does not claim

No measurement of this correction in any real quantum channel is claimed. No claim that the golden ratio is the only possible source of a finite-N correction. No claim that the framework's derivation of the golden ratio is physically validated.

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