pith. machine review for the scientific record. sign in
structure definition def or abbrev high

QuantumChannelCapacityCert

show as:
view Lean formalization →

The quantum channel capacity correction certificate is a structure that bundles three properties of the phi-ladder correction term 1/(phi N): positivity for all positive block lengths N, strict decrease as N increases, and an upper bound of 1/N. Quantum information researchers modeling finite-size effects in entanglement-assisted channels would cite this when confirming the RS correction rate. The structure definition itself requires no proof steps and is populated by direct references to the supporting positivity, decrease, and bound lemmas.

claimLet $c(N) := 1/ (phi N)$ denote the finite-N correction to quantum channel capacity for positive integers $N$. A certificate for this correction is a structure asserting that $c(N) > 0$, that $c(N+1) < c(N)$, and that $c(N) leq 1/N$.

background

The module develops finite-N corrections to quantum channel capacity arising from the phi-ladder in Recognition Science. The classical Shannon capacity is log base 2 of (1 + S/N). The quantum analog incorporates an RS correction scaling as log base 2 of (1 + 1/(phi N)) per input symbol, where phi is the golden ratio fixed point. The correction function is defined as 1/(phi N) for N positive. Its positivity follows from the positivity of phi and of N, as shown in the upstream positivity theorem for the correction. This setting predicts that the ratio of entanglement-assisted to classical capacity for N-symbol blocks is 1 + 1/(phi N), with the correction term decaying as 1/N rather than 1/N squared.

proof idea

The declaration defines a structure whose three fields directly encode the required properties of the correction. No internal proof is performed; the structure serves as a type that collects the positivity assertion, the strict decrease statement, and the inverse bound. Downstream instantiation supplies the concrete lemmas for each field.

why it matters in Recognition Science

This certificate earns its place by providing a reusable interface for the phi-ladder correction properties in quantum information. It is instantiated in the concrete certificate definition that packages the full set of verified inequalities. The construction aligns with the module's structural prediction that the correction vanishes linearly in 1/N, a rate distinguishable from classical models with no finite-N term. It draws on the phi fixed point from the self-similar forcing chain but does not invoke the full T0-T8 sequence here.

scope and limits

formal statement (Lean)

  72structure QuantumChannelCapacityCert where
  73  correction_pos : ∀ {N : ℕ} (hN : 0 < N), 0 < correction N hN
  74  strictly_decreasing :
  75    ∀ (N : ℕ) (hN : 0 < N),
  76      correction (N + 1) (Nat.succ_pos _) < correction N hN
  77  bounded_by_inv :
  78    ∀ {N : ℕ} (hN : 0 < N), correction N hN ≤ 1 / (N : ℝ)
  79
  80/-- Quantum-channel-capacity correction certificate. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.