Information Quantum Channel Capacity From Phi Quantum Channel Capacity Cert

The finite-N correction certificate

In the classical theory of communication, the Shannon capacity of a noisy channel is the maximum rate at which information can be sent reliably. For a channel with signal-to-noise ratio S/N, the formula is C = log₂(1 + S/N). Quantum channels, where information is carried in quantum states, have their own capacity measures, such as the entanglement-assisted capacity, which can exceed the classical limit. The Recognition Science framework, a body of work that derives physical structure from a forced cost function, introduces a finite-size correction to these quantum capacities.

The correction is expressed in terms of the golden ratio φ, a number that appears throughout the framework. For a block of N input symbols, the correction factor is defined as 1 / (φ · N). This factor is not a free parameter; it is the same φ-suppressed correction that the framework's formal library already derives for the classical Shannon bound. The structural prediction is that the ratio of entanglement-assisted capacity to classical capacity for an N-symbol block is 1 + 1/(φ·N).

What the machine-checked declaration QuantumChannelCapacityCert establishes is narrower and precise. It packages three provable properties of the correction factor. First, the correction is strictly positive for every positive N. Second, it strictly decreases as N grows, so a larger block always carries a smaller correction. Third, it is bounded above by 1/N, meaning it vanishes at least as fast as 1/N as N goes to infinity. These three properties are proved in the framework's library of formal theorems, with no unproved assumptions.

In Recognition Science, this certificate is a structural claim about how quantum capacities behave at finite block sizes. The correction vanishing as 1/N, rather than 1/N², is a signature that distinguishes this model from any classical-only model that has no finite-N correction at all. The certificate does not, however, prove the full capacity formula, nor does it establish that the ratio prediction 1 + 1/(φ·N) is empirically true for real quantum channels. It certifies only the shape and decay of the correction term, not its physical realization.

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

The certificate does not prove the full quantum channel capacity formula, only the properties of the correction factor. The certificate does not establish that the ratio prediction 1 + 1/(φ·N) holds for real physical quantum channels. The certificate does not claim the correction is unique or that no other correction term is possible.

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: