cert_inhabited
plain-language theorem explainer
Existence of an LDPC certificate: domain cost vanishes at equal nonzero rates, is nonnegative on positive rates, and the canonical threshold is strictly positive. Cited by anyone packaging the J-cost LDPC rate gap as a reusable certificate object. Term proof: inhabit Nonempty by the concrete witness cert.
Claim. The type of LDPC certificates is inhabited: there exists a witness that the domain cost $C(m,e)$ satisfies $C(r,r)=0$ for all $r\neq 0$, $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and the canonical threshold is strictly positive.
background
This module packages a structural claim about LDPC code rates in Recognition Science units. The empirical target is that practical LDPC codes sit a fixed gap below Shannon capacity, identified with the J-cost at the golden ratio: $J(\varphi)\approx 0.118$ (about an 11.8% finite-blocklength penalty).
Domain cost is the local cost functional on message and error rate parameters. At equilibrium (equal nonzero rates) it vanishes; off equilibrium it stays nonnegative. The canonical threshold is the positive scalar used as the designed-rate cutoff in this certificate.
LDPCCert is the structure bundling those three properties: equilibrium vanishing, nonnegativity, and positive threshold. The sibling cert is a concrete inhabitant built from the corresponding lemmas on domain cost and the threshold.
proof idea
One-line term proof. Nonempty LDPCCert is inhabited by the anonymous constructor ⟨cert⟩, i.e. the already-constructed certificate value is the witness. No tactics, no further lemmas at the call site.
why it matters
Closes the certificate layer for the LDPC-from-J-cost story in the Information domain: once LDPCCert is nonempty, downstream developments can assume a single packaged witness rather than re-proving equilibrium vanishing, nonnegativity, and threshold positivity separately.
The module frames this as a structural theorem (zero sorry, zero axiom) tying the Recognition J-cost at $\varphi$ to the observed LDPC gap below Shannon capacity. No downstream consumers are wired yet in the graph; the declaration is the existence seal on the local certificate bundle rather than a step in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.