gapAt_pos
plain-language theorem explainer
The declaration proves that the gap-to-capacity function remains strictly positive for every natural-number rung k on the phi-ladder. Information theorists working with finite-length polar-code bounds in the Recognition Science setting would cite this result to guarantee well-defined ratios in adjacent-rung comparisons. The proof is a direct algebraic reduction that unfolds the definition and invokes positivity of real powers together with linear arithmetic.
Claim. For every natural number $k$, the gap-to-capacity satisfies $gapAt(k) > 0$, where $gapAt(k) := phi^{-k}$ with the reference gap normalized to 1.
background
The module places polar-code gap-to-capacity on the phi-ladder, where adjacent gaps decay by the factor $phi^{-1}$. The function gapAt is defined as referenceGap times phi to the power minus k, with referenceGap equal to 1. This mirrors the structure used in athletic record progression and quantum channel capacity corrections. The upstream Constants structure supplies the positivity of phi required for the power.
proof idea
The proof unfolds the definitions of gapAt and referenceGap, yielding phi raised to minus k. It then applies zpow_pos using Constants.phi_pos to obtain the strict inequality, and finishes with linarith.
why it matters
This result supplies the positivity hypothesis for the polarCodeCert definition and for the adjacent-ratio theorem that follows. It anchors the information-theoretic side of the phi-ladder construction, consistent with the same decay structure appearing in record-progression fits. The certificate polarCodeCert packages gap_pos, one_step_ratio, and adjacent_ratio for downstream use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.