DataCompr3Cert
plain-language theorem explainer
Certificate structure packing three structural properties of domain cost used for optimal RS data compression: diagonal vanishing, non-negativity off the identity, and a strictly positive canonical threshold. Downstream code cites the inhabited instance and the concrete cert packing. Pure structure definition with no proof body.
Claim. A data-compression certificate is a triple of properties: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module develops optimal data compression from the Recognition Science J-cost. In classical coding, Huffman codes achieve average length between $H(X)$ and $H(X)+1$ bits. Here the claim is structural: an optimal RS encoding incurs $J(\varphi)$ bits of overhead per symbol beyond Shannon entropy, with $J(x)=(x+x^{-1})/2-1$.
Domain cost is the local cost functional on pairs of positive reals (message and encoding scales) built from that J-cost. The canonical threshold is the positive cutoff used to separate compressible from incompressible regimes. Upstream, recognition-event cost is already known to be nonnegative via $J$-cost nonnegativity on positive states.
This structure does not compute compression rates; it only names the three algebraic properties the later certificate must discharge.
proof idea
No proof body: the declaration is a structure (record type) with three fields. Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos, and to cert_inhabited, which wraps that instance as Nonempty.
why it matters
Gives a single named interface for the three cost axioms needed by the Plan v7 data-compression development. Downstream, cert is the concrete zero-sorry packing of those axioms, and cert_inhabited records that the certificate type is nonempty. That closes the structural half of the module claim (0 sorry, 0 axiom) that RS optimal encoding is controlled by J-cost geometry, including the $J(\varphi)$ overhead relative to Shannon. Ties to the broader forcing picture only indirectly: nonnegativity of cost is the same J-cost positivity used in observer forcing and the T5 uniqueness of $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.