DataCompr3DeepCert
plain-language theorem explainer
Certificate packing three structural facts for J-cost data compression: diagonal domain cost vanishes, cost is nonnegative on positive arguments, and the canonical threshold is positive. Consumers of the RS compression-rate bound cite it via the inhabited instance. Pure structure definition with no proof body.
Claim. A data-compression certificate consists of three properties: (i) for every nonzero real $r$, the domain cost of $r$ against itself is zero; (ii) for all positive reals $m,e$, the domain cost of $m$ against $e$ is nonnegative; (iii) the canonical compression threshold is strictly positive.
background
The module derives an RS data-compression rate from the J-cost. Classical Shannon coding needs $H$ bits per symbol; the RS claim adds a fixed overhead $J(\varphi)$ per symbol, so at $H=1$ the average length is about $1.118$ bits/symbol. Status is structural (zero sorry, zero axiom).
Domain cost is the local cost functional on a measure/evidence pair, built from the Recognition Science J-cost $J(x)=(x+x^{-1})/2-1$. The diagonal identity $J(1)=0$ forces vanishing self-cost. Nonnegativity of recognition cost is the standard J-cost fact: every recognition event has cost $\ge 0$ (ObserverForcing).
The canonical threshold is the positive cutoff used to separate compressible from incompressible regimes in the three-deep compression argument.
proof idea
No proof body: this is a structure declaration. It only names the three fields that any inhabiting certificate must supply (diagonal vanishing, nonnegativity, positive threshold). Downstream cert fills those fields with the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the typed interface for the module's compression certificate. Downstream cert builds a concrete inhabitant, and cert_inhabited records Nonempty of the structure, closing the structural theorem announced in the module doc.
In the broader framework this sits in the Information layer that converts J-cost (T5 uniqueness, RCL) into an operational coding overhead $J(\varphi)$. It does not itself compute the numerical rate; it packages the cost axioms the rate argument needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.