gap_times_N_invariant
plain-language theorem explainer
Gap to capacity times block length N equals 1/φ for every positive real N. LDPC code analysts would cite the invariance to forecast how the finite-length penalty shrinks with larger blocks. The argument is a direct algebraic reduction once the explicit gap definition is substituted.
Claim. For every real number $N > 0$, if $g(N)$ denotes the gap to Shannon capacity at block length $N$, then $g(N) · N = φ^{-1}$.
background
The LDPC module treats the finite-blocklength correction to Shannon capacity as a φ-suppressed gap. The upstream definition states: 'Gap to Shannon capacity for an LDPC code of block length N.' It is given explicitly by $g(N) = 1/(φ N)$. The local setting assumes LDPC Tanner graphs whose variable-node mean degree is at least 3, check-node mean degree at least 4, and girth at least 6 so that belief propagation meets this gap.
proof idea
Unfold the definition of gapToCapacity. Derive $N ≠ 0$ from the positivity hypothesis. Apply field simplification to cancel the common factors and obtain the constant 1/φ.
why it matters
The result is packaged inside the LDPCRateCert structure that bundles positivity, monotonicity, doubling, and invariance of the gap. It directly records the φ-suppression law for LDPC codes, linking to the Recognition Science derivation of constants via the phi-ladder. The module falsifier is any stable LDPC code whose gap deviates from the 1/(φ N) scaling at moderate block lengths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.