LDPCCert
plain-language theorem explainer
Certificate packaging three analytic facts used by the LDPC rate-from-J-cost argument: domain cost vanishes on the diagonal, is nonnegative off equilibrium, and the canonical threshold is positive. Anyone wiring the Shannon-gap claim through J-cost cites this bundle. It is a pure structure definition with no proof body; inhabitants supply the three fields.
Claim. An LDPC certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost at equal arguments vanishes, $\mathrm{domainCost}(r,r)=0$; (ii) for positive message and error rates $m,e>0$, $\mathrm{domainCost}(m,e)\ge 0$; (iii) the canonical threshold is strictly positive.
background
The module treats the empirical gap between designed LDPC rate and Shannon capacity as a J-cost penalty. In Recognition Science the cost functional is $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), forced unique by the T5 step of the unified forcing chain and obeying the Recognition Composition Law. The module introduces a domain-level cost on message/error rates whose equilibrium value is zero and whose positivity away from equilibrium mirrors the nonnegativity of recognition-event cost.
Upstream, cost_nonneg states that every recognition event has nonnegative cost, proved from nonnegativity of $J$ on positive reals. The canonical threshold is the positive scale (tied to $J(\varphi)\approx 0.118$) against which finite-blocklength LDPC capacity penalty is compared. The local setting is structural: zero sorry, zero axioms, packaging only the analytic hypotheses the rate claim needs.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Downstream, the concrete inhabitant fills them by applying the sibling lemmas domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named interface for the analytic side conditions of the LDPC-from-J-cost story. Downstream, cert is the canonical inhabitant and cert_inhabited records that the type is nonempty. The module doc frames the physics claim: well-designed LDPC codes sit within about 5–15% of Shannon capacity, with the Recognition-native gap scale $J(\varphi)\approx 0.118$ (the T5/T6 cost at the golden fixed point). Packaging the three facts keeps the rate theorem free of scattered side conditions and ties information-theoretic coding performance to the same J-cost that forces $\varphi$ and the eight-tick octave elsewhere in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.