correction_pos
plain-language theorem explainer
The theorem establishes that the finite-N correction factor 1/(phi N) remains strictly positive for every positive integer N. Researchers working on quantum channel capacities in the Recognition Science framework would cite this to confirm the correction never vanishes or becomes negative at finite block sizes. The proof is a short tactic script that unfolds the definition, pulls positivity of phi from the Constants bundle, casts the natural number to reals, and invokes the positivity tactic.
Claim. For every positive integer $N$, the correction term $1/ (phi N)$ is strictly positive, where $phi$ is the positive real constant from the CPM constants structure.
background
The module formalizes a phi-suppressed correction to quantum channel capacity that scales as log2(1 + 1/(phi N)) per symbol, matching the RS finite-N adjustment already present in the classical Shannon bound. The correction function is defined directly as 1 / (phi * N) in the reals. Upstream, the Constants structure from LawOfExistence supplies the positivity of phi, while the from theorem in PrimitiveDistinction derives the required structural conditions from seven axioms. The local setting is the finite-N correction to entanglement-assisted capacity that vanishes as 1/N.
proof idea
The proof unfolds the definition of correction, obtains 0 < phi from Constants.phi_pos, casts the hypothesis 0 < N to a real inequality via exact_mod_cast, and applies the positivity tactic.
why it matters
This result supplies the positivity field required by the QuantumChannelCapacityCert structure, which is then instantiated in quantumChannelCapacityCert. It closes the positivity requirement in the certificate for the phi-ladder correction to quantum channel capacity, consistent with the RS prediction that the correction vanishes as 1/N. It supports the T6 phi fixed-point and T7 eight-tick octave landmarks by ensuring the correction term remains well-behaved for all finite N.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.