gap_at_10k_eq
plain-language theorem explainer
The equality fixes the gap to capacity at block length 10000 as exactly 1 over phi times 10000. Information theorists verifying LDPC performance against the 0.5 dB empirical benchmark at N=10000 would cite this specialization. The proof is a one-line reflexivity that unfolds the definition of gapAt10k.
Claim. Let $g(N)$ denote the gap to capacity for an $N$-bit LDPC code under the phi-suppression law. Then $g(10000) = 1/ (phi * 10000)$.
background
The module derives LDPC code rates from the phi-suppression law proved in ShannonAsJCostLimit, where the finite-N correction to Shannon capacity is $g(N) = 1/(phi N)$. gapAt10k is the specialization of gapToCapacity at N=10000, chosen because it reproduces the observed ~0.5 dB gap for industry codes. phi is the self-similar fixed point from the Recognition forcing chain (T6).
proof idea
The proof is a direct reflexivity. gapAt10k is defined as gapToCapacity 10000, and the general gap formula supplies the right-hand side 1/(phi * 10000).
why it matters
This pins the numerical value at the representative block length N=10000 used in 5G and Wi-Fi LDPC designs. It supports the LDPCRateCert construction in the same module and closes the link between the abstract J-cost limit and concrete code metrics. The result relies on the phi-suppression law from the upstream gapToCapacity definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.