gapAt_adjacent_ratio
plain-language theorem explainer
The theorem establishes that the gap-to-capacity at consecutive rungs on the phi-ladder for polar codes satisfies the fixed ratio 1/phi. Information theorists deriving finite-length scaling for polar codes would cite this when chaining decay across block lengths. The proof is a direct reduction that rewrites via the successor relation and clears the denominator with the positivity witness.
Claim. For every natural number $k$, the ratio of gaps satisfies $gapAt(k+1)/gapAt(k)=phi^{-1}$, where $gapAt(k)$ denotes the gap-to-capacity at rung $k$ on the phi-ladder, defined by $gapAt(k) := referenceGap · phi^{-k}$.
background
The module places polar-code finite-length gaps on the phi-ladder, with the explicit definition gapAt k := referenceGap * phi^(-(k:ℤ)). This is the identical construction used for record-progression gaps in the Sport module. The local setting states that polar codes achieve capacity with gap O(2^{-N^{0.5}}), yet the adjacent-rung ratio is fixed at 1/phi, matching the structure already obtained for quantum-channel-capacity corrections.
proof idea
The proof is a one-line wrapper. It rewrites the left-hand side by the successor-ratio lemma gapAt_succ_ratio, which expands gapAt(k+1) into gapAt k * phi^{-1}, then applies field_simp using the non-zero witness supplied by gapAt_pos k to cancel the common factor.
why it matters
This supplies the adjacent_ratio field required by the polarCodeCert certificate, which bundles positivity, successor, and adjacent properties into one structure. It realizes the module claim that the same 1/phi factor governs polar-code gaps, quantum-channel corrections, and LDPC rate gaps. In the Recognition framework it instantiates the self-similar fixed-point property of phi on the information side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.