cert
plain-language theorem explainer
Packages three elementary properties of the domain cost into a single certificate for the J-cost data-compression story: diagonal vanishing, nonnegativity on positive arguments, and a positive canonical threshold. Anyone citing the structural compression theorem in this module will pull this bundle. The body is a pure structure instance that wires 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 develops optimal data compression from the Recognition Science J-cost. Classical Huffman coding places average code length between $H(X)$ and $H(X)+1$ bits; the RS claim is that an optimal recognition encoding incurs $J(\varphi)$ bits of overhead per symbol beyond Shannon entropy.
Domain cost is the local cost functional on pairs of positive reals used as the compression score. The certificate structure DataCompr3Cert packages the three algebraic facts needed downstream: the cost vanishes when measure and estimate coincide (off zero), it is nonnegative on the positive orthant, and the canonical threshold used to cut codes is positive.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing: every recognition event has cost $0\le e.\mathrm{cost}$, via nonnegativity of $J$.
proof idea
One-line structure instance. The three fields of the certificate are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra rewriting or case analysis.
why it matters
This is the inhabited certificate that closes the structural half of "Optimal Data Compression from J-Cost" (module status: 0 sorry, 0 axiom). It sits under the information-domain claim that RS encoding overhead is controlled by $J(\varphi)$, tying compression back to the unique J-cost forced at T5 and the golden ratio fixed point at T6.
No downstream consumers are recorded yet in the graph; the certificate is the export surface for later compression or coding theorems that need a single named bundle of cost axioms rather than three separate lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.