correction_strictly_decreasing
plain-language theorem explainer
Recognition Science supplies a strictly decreasing finite-N correction 1/(phi N) to quantum channel capacity as block length grows from N to N+1. Researchers in quantum information citing RS corrections for capacity bounds would reference this monotonicity. The proof reduces the claim to the reciprocal being strictly decreasing on positives after unfolding the definition and verifying the argument increases.
Claim. For every positive integer $N$, let $c(N) := 1/ (phi · N)$. Then $c(N+1) < c(N)$.
background
The module formalizes a phi-suppressed finite-N correction to quantum channel capacity. The correction is defined as 1/(phi N) for positive integer input-symbol count N. This term modifies the classical Shannon capacity to produce the entanglement-assisted-to-classical ratio 1 + 1/(phi N), with the correction vanishing as 1/N rather than 1/N².
proof idea
The proof unfolds the definition of correction. It obtains phi > 0 from Constants.phi_pos, casts N and N+1 to positive reals, and shows phi N < phi (N+1) via mul_lt_mul_of_pos_left applied to N < N+1. The inequality 1/(phi (N+1)) < 1/(phi N) then follows directly from one_div_lt_one_div_of_lt.
why it matters
The result is referenced inside the quantumChannelCapacityCert definition to bundle positivity, strict decrease, and the 1/N bound. It fills the module's structural prediction that adjacent-N capacity ratios differ by a term of order 1/phi, distinguishing the RS correction from classical models. This step aligns with the phi fixed point in the forcing chain and the J-cost information bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.