cert
plain-language theorem explainer
Packages three elementary facts about the RS domain cost and threshold into a single compression-ratio certificate. Anyone citing the RS claim that structured data compresses by J(φ)^{-1} ≈ 8.47× needs this witness. The definition is a pure structure instance wiring three sibling lemmas; no new mathematics is proved here.
Claim. There is a compression-ratio certificate asserting: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for all $r\neq 0$; (ii) the domain cost is nonnegative for positive model and evidence arguments; (iii) the canonical compression threshold is strictly positive.
background
The module treats maximum lossless compression in Recognition Science terms. The Kolmogorov limit is restated as an RS cost bound: structured data at φ-rung complexity is compressible by $J(\varphi)^{-1}\approx 8.47\times$, while random data remains incompressible (factor $1\times$). Status is structural (no sorry, no axioms).
The certificate structure CompressionRatioCert packages three Prop fields: diagonal vanishing of the domain cost, nonnegativity of that cost on the positive orthant, and positivity of the canonical threshold. Domain cost is the local cost functional used to score model-versus-evidence mismatch; it is built from the standard J-cost $J(x)=(x+x^{-1})/2-1$ of the forcing chain (T5).
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing (cost_nonneg: every recognition event has nonnegative cost via Jcost_nonneg). The present certificate lifts the analogous nonnegativity statement to the information-theoretic domain-cost interface.
proof idea
One-line structure instance. The three fields of CompressionRatioCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity on positive arguments), and canonicalThreshold_pos (threshold positivity). No tactics or algebraic work occur in the body; the definition is pure wiring.
why it matters
This certificate is the inhabited witness that the RS compression-ratio interface is well-formed. The module frames achievable lossless compression as $J(\varphi)^{-1}$ for structured φ-rung data, tying the information bound to the unique J-cost forced at T5 and to φ as the self-similar fixed point (T6). Without a positive threshold and a nonnegative diagonal-vanishing cost, the numerical 8.47× claim has no certified carrier.
No downstream consumers are recorded yet (used_by empty), so the declaration currently closes the local certificate API rather than feeding a larger theorem. It sits beside cert_inhabited and the domain-cost lemmas as scaffolding for any later theorem that quotes the Kolmogorov-style RS compression bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.