gap_at_10k_pos
plain-language theorem explainer
The declaration proves that the gap-to-capacity function evaluated at block length 10000 is strictly positive. Researchers modeling LDPC performance in 5G and Wi-Fi would reference it to anchor the φ-suppression prediction at a representative industry block length. The proof reduces immediately to the general positivity lemma for the gap function by unfolding the definition and supplying a trivial positivity witness for 10000.
Claim. Let $g(N)$ denote the gap to Shannon capacity at block length $N$. Then $0 < g(10000)$.
background
In the LDPC module the gap-to-capacity is introduced as the finite-N correction $g(N) = 1/ (φ N)$ derived from the J-cost limit. The upstream theorem gap_pos states that $0 < g(N)$ whenever $N > 0$, proved by showing the denominator φN remains positive. gapAt10k is the concrete instance gapToCapacity 10000, chosen because empirical LDPC codes at this length exhibit a measured gap near 0.5 dB, matching 1/φ^5.
proof idea
The proof is a one-line wrapper. It unfolds gapAt10k to expose gapToCapacity 10000, then applies the general positivity result gap_pos at that specific N, discharging the hypothesis 0 < 10000 via norm_num.
why it matters
The result supplies the positivity check required by the module's φ-suppression law for LDPC codes at a standard block length. It directly supports the claims that the gap is monotone decreasing, halves on doubling N, and remains positive for all N > 0. The parent statements are gap_pos and the definition gapAt10k; the module doc flags the falsifier as any corpus of LDPC codes whose measured gap deviates from the 1/(φN) scaling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.