cert_inhabited
plain-language theorem explainer
The certificate bundle for three-deep error-correction capacity derived from J-cost is nonempty: there exists a witness packing the zero-on-diagonal, nonnegativity, and positive-threshold facts. Information theorists citing the RS Hamming-bound rate R = J(φ) ≈ 0.118 use this to discharge existence. The proof is a one-line term inhabitation via the concrete certificate value.
Claim. The type of certificates asserting (i) domain cost vanishes on the diagonal $r\neq 0\Rightarrow C(r,r)=0$, (ii) domain cost is nonnegative for positive arguments, and (iii) the canonical threshold is strictly positive, is nonempty.
background
The module derives a structural Hamming-bound statement from the Recognition Science J-cost: at rate $R=J(\varphi)\approx 0.118$ a code supports error fraction $t/n=J(\varphi)/2\approx 0.059$. The bound is $2^{n-k}\ge V_H(n,t)$ with $V_H$ the Hamming ball volume; the argument is purely structural (zero sorry, zero axiom).
Domain cost is the local cost functional on message/error pairs used to encode the J-cost geometry. The canonical threshold is the positive cutoff against which correctability is measured. The certificate structure packages three elementary properties: cost vanishes when message equals error scale, cost is nonnegative on the positive orthant, and the threshold is positive.
These three facts are the minimal algebraic interface needed before any rate or capacity comparison is stated.
proof idea
One-line term proof. The concrete value cert already assembles the three fields of the certificate structure, so Nonempty is inhabited by the anonymous constructor ⟨cert⟩. No tactics, no further lemmas.
why it matters
Closes the existence obligation for the three-deep error-correction certificate in the Information layer. Downstream consumers that quantify over such certificates (rate bounds, capacity comparisons at $R=J(\varphi)$) can invoke nonempty rather than reconstruct the witness. Ties directly to the module claim that RS forces a concrete correctable error fraction $t/n=J(\varphi)/2$ from the same J that appears in the forcing chain (T5 J-uniqueness, T6 $\varphi$ fixed point). No further used-by edges are recorded yet; the declaration is the terminal existence seal of the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.