cert
plain-language theorem explainer
Packages three structural facts about the domain J-cost (vanishes on the equal-rate diagonal, is nonnegative for positive rates, and the canonical threshold is positive) into one LDPC certificate record. Cited by anyone treating the J-cost gap as an LDPC rate-to-capacity penalty. Construction is a direct field-wise assembly of three already-proved lemmas; no new argument.
Claim. There is a certificate asserting: (i) the domain cost of equal nonzero rates vanishes, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module treats LDPC code rate relative to Shannon capacity through the Recognition Science cost functional. Empirically, well-designed LDPC codes sit within about 5–15% of capacity; the RS claim is that the structural gap is set by $J(\varphi)\approx 0.118$, i.e. an 11.8% finite-blocklength penalty.
Domain cost is the two-argument cost on message and evidence rates built from the unique J-cost $J(x)=(x+x^{-1})/2-1$ (forced at T5). It is zero when the two rates coincide and nonnegative off the diagonal. The canonical threshold is the positive scale against which that gap is read.
Upstream, nonnegativity of recognition cost is already known: every recognition event has cost $\ge 0$ because $J$ itself is nonnegative on positive reals. The certificate structure simply records the three properties needed to treat domain cost as a legitimate LDPC rate certificate.
proof idea
One-line structure inhabitant. The three fields of LDPCCert are filled by the sibling lemmas already in the module: equilibrium vanishing supplies the diagonal identity, domain-cost nonnegativity supplies the sign bound, and positivity of the canonical threshold supplies the last field. No tactics beyond record construction; no new inequalities are proved here.
why it matters
Gives a single named witness that the J-cost apparatus is admissible as an LDPC rate certificate. Downstream consumers can quote one object instead of three separate lemmas when arguing that the designed-rate gap is controlled by $J(\varphi)$. That gap is the information-theoretic reading of the unique cost forced at T5 in the forcing chain, with $\varphi$ the self-similar fixed point from T6.
The module is marked structural (zero sorry, zero axiom). This definition closes the certificate interface so later rate-threshold theorems can assume a single inhabited record rather than re-proving cost axioms. No parent theorems yet depend on it (used_by is empty), so it is infrastructure for the LDPC–Shannon gap story rather than a leaf result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.