correction_le_inv
plain-language theorem explainer
The bound shows that the phi-ladder correction to quantum channel capacity is at most 1/N for any positive integer block length N. Information theorists comparing finite-blocklength quantum capacities to classical Shannon limits would cite the result to bound the suppression factor. The proof unfolds the definition of the correction and applies the reciprocal inequality after establishing phi greater than 1.5.
Claim. For every positive integer $N$, the phi-ladder finite-$N$ correction factor satisfies $1/ (phi N) leq 1/N$.
background
The module develops a finite-blocklength correction to quantum channel capacity that arises from the phi-ladder of Recognition Science. The correction term is defined as 1 over phi times N for positive integer N; it enters the entanglement-assisted capacity ratio as the additive factor 1 over phi N and is required to vanish as 1/N. The local theoretical setting is the quantum analog of the classical Shannon capacity C equals log base 2 of 1 plus S/N, now equipped with the RS phi-suppressed term already formalized in the Shannon-as-J-cost limit.
proof idea
The tactic proof first unfolds the definition of the correction to reach 1 over phi N. It invokes the upstream lemma phi greater than 1.5 to obtain phi greater than 1, derives the positivity facts 0 less than N and 0 less than phi N, establishes the comparison N less than or equal to phi N by right-multiplication, and finishes with the standard reciprocal inequality one_div_le_one_div_of_le on positive reals.
why it matters
The inequality is packaged inside the quantumChannelCapacityCert structure that certifies all required correction properties for the quantum capacity formula. It supplies the concrete 1/N upper bound needed to distinguish the RS prediction (vanishing as 1/N) from any classical-only model that carries zero finite-N correction. The result therefore closes one of the elementary bounds required by the phi-ladder construction in the Information domain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.