LDPCRateCert
plain-language theorem explainer
LDPCRateCert bundles four properties of the gap-to-capacity function g(N) = 1/(phi N) for LDPC codes: positivity for N > 0, strict decrease with growing N, exact halving upon doubling N, and the invariant g(N) * N = 1/phi. Coding theorists studying finite-blocklength corrections would cite the certificate to confirm phi-suppression matches observed LDPC gaps. The declaration is a pure structure definition that packages upstream lemmas without further reasoning steps.
Claim. A certificate for the LDPC gap-to-capacity function is a structure whose fields assert that g(N) := 1/(phi N) satisfies g(N) > 0 for every N > 0, is strictly monotone decreasing, obeys g(2N) = g(N)/2, and fulfills the scaling invariance g(N) * N = 1/phi.
background
In the LDPC code-rate module the gap-to-capacity for block length N is defined by gapToCapacity N := 1/(phi * N). This expression encodes the finite-N correction to Shannon capacity derived from the J-cost limit in the upstream ShannonAsJCostLimit result. The module assumes LDPC codes with mean variable-node degree at least 3, check-node degree at least 4, and Tanner-graph girth at least 6 achieve this gap under belief-propagation decoding.
proof idea
The declaration is a structure definition with an empty proof body. It simply collects the four fields, which are later supplied by the sibling theorems gap_pos, gap_decreasing, gap_doubling_halves, and gap_times_N_invariant when the downstream cert instance is constructed.
why it matters
LDPCRateCert supplies the bundled object instantiated by the downstream cert definition, allowing the phi-suppression law g(N) = 1/(phi N) to be referenced as a single certificate in larger arguments. It directly fills the module's claim that LDPC gaps are positive, monotone, and scale by exact halving on doubling N. Within Recognition Science this links the information gap to the phi fixed point and the eight-tick octave, since the doubling relation corresponds to one step in the 2^3 period.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.