gap_doubling_halves
plain-language theorem explainer
The gap-to-capacity function for LDPC block codes satisfies g(2N) = g(N)/2 for every N > 0. Information theorists modeling finite-length performance in 5G and Wi-Fi standards would cite this exact scaling. The proof is a direct algebraic reduction: unfold the explicit formula, invoke phi nonzero, and apply field simplification.
Claim. Let $g(N) := 1/ (phi N)$ denote the gap to Shannon capacity for an LDPC code of block length $N > 0$. Then $g(2N) = g(N)/2$.
background
The LDPCCodeRateFromPhi module encodes the phi-suppressed gap-to-capacity law for low-density parity-check codes. gapToCapacity is defined explicitly as 1/(phi * N), where phi is the golden ratio. This supplies the finite-N correction to Shannon capacity under the degree and girth conditions stated in the module documentation. Upstream, phi_ne_zero supplies the non-vanishing fact required for all divisions involving phi.
proof idea
Unfold gapToCapacity on both sides of the target equality. Obtain phi ≠ 0 from phi_ne_zero and N ≠ 0 from the positivity hypothesis via ne_of_gt. Apply field_simp to cancel the common phi and N factors.
why it matters
The result populates the doubling_halves field inside the LDPCRateCert record, which collects the four core properties of the gap function. It completes the scaling claim listed in the module documentation for the phi-suppressed gap argument. In the Recognition Science setting it reinforces the appearance of phi in information bounds, consistent with the same suppression factor used in the gap and mass derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.