cert
plain-language theorem explainer
Packages three elementary properties of the domain cost (vanishes on the diagonal, is nonnegative for positive arguments, and has a positive canonical threshold) into a single certificate structure for the 3-deep J-cost compression claim. Anyone citing the RS overhead H + J(φ) bits/symbol will point here for the structural bundle. The body is a pure structure instance wiring three sibling lemmas.
Claim. There is a certificate recording that the domain cost $C$ satisfies $C(r,r)=0$ for all $r\neq 0$, that $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and that the canonical compression threshold is strictly positive.
background
The module treats data compression as a recognition-cost problem. Shannon's optimum is $H$ bits per symbol; Recognition Science adds a forced overhead $J(\varphi)$ from the unique cost functional $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), so an RS-optimal code averages $H+J(\varphi)$ bits/symbol. At one bit of source entropy this is about $1.118$ bits/symbol.
The domain cost is the local cost comparison between a measure $m$ and an estimate $e$. The certificate structure DataCompr3DeepCert packages the three structural facts needed downstream: the cost vanishes when measure equals estimate, stays nonnegative on the positive quadrant, and the canonical threshold used to cut the code is positive. Upstream, nonnegativity of recognition-event cost is already forced by $J\ge 0$ on positive reals.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas that already prove diagonal vanishing of the domain cost, its nonnegativity for positive arguments, and positivity of the canonical threshold. No extra algebra is performed at this site.
why it matters
This is the inhabited certificate that closes the structural side of the 3-deep compression theorem in the Information domain. The module is marked structural (zero sorry, zero axiom) and records the RS claim that optimal codes carry an irreducible $J(\varphi)$ overhead on top of entropy. The certificate is the single object a later theorem can assume when it needs all three cost properties at once. It sits downstream of the J-cost nonnegativity forced in the observer/forcing layer (T5 uniqueness of $J$) and feeds any argument that quotes the $H+J(\varphi)$ rate. No further used-by edges are recorded yet; the companion inhabitedness lemma is the immediate consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.