cert
cert constructs the LDPCRateCert structure by supplying the four required properties of the gap-to-capacity function. Information theorists studying finite-blocklength LDPC performance would cite it to access the full set of φ-suppression laws in one object. The definition is a direct field assignment from the theorems gap_pos, gap_decreasing, gap_doubling_halves, and gap_times_N_invariant.
claimLet $g(N) = 1/ (phi N)$ for real $N > 0$. Then cert is the structure asserting $g(N) > 0$, that $g$ is strictly decreasing, that $g(2N) = g(N)/2$, and that $g(N) · N = 1/phi$.
background
In the LDPCCodeRateFromPhi module the gap-to-capacity function is defined as gapToCapacity N := 1 / (phi * N). The structure LDPCRateCert collects four properties: positivity of the gap for positive block length, strict monotonic decrease with N, exact halving upon doubling N, and the invariant product gap(N) * N = 1/phi. These properties are established individually by the theorems gap_pos, gap_decreasing, gap_doubling_halves, and gap_times_N_invariant. The module situates this within the broader Recognition Science claim that the finite-N correction to Shannon capacity is 1/(φN) for LDPC codes satisfying standard degree and girth conditions.
proof idea
The definition cert is a one-line wrapper that populates the LDPCRateCert structure by direct assignment of its four fields to the corresponding theorems gap_pos, gap_decreasing, gap_doubling_halves, and gap_times_N_invariant.
why it matters in Recognition Science
cert provides the packaged certificate for the φ-suppressed gap-to-capacity law in LDPC codes, completing the local development outlined in the module documentation. It consolidates the results that support the empirical observation of gaps near 1/φ^5 at N ≈ 10,000. Within the Recognition framework this supplies the information-theoretic component of the B16 deepening, linking the J-cost limit to practical error-correction performance.
scope and limits
- Does not prove that any concrete LDPC code achieves the predicted gap.
- Does not apply the gap law to non-LDPC code families.
- Does not incorporate the specific degree-distribution or girth constraints on the Tanner graph.
- Does not address decoding complexity or implementation details.
formal statement (Lean)
101def cert : LDPCRateCert where
102 gap_pos := gap_pos
proof body
Definition body.
103 gap_monotone := gap_decreasing
104 doubling_halves := gap_doubling_halves
105 gap_N_invariant := gap_times_N_invariant
106
107end
108
109end LDPCCodeRateFromPhi
110end Information
111end IndisputableMonolith