CompressionRatioCert
plain-language theorem explainer
Certificate structure bundling three facts that make the RS compression ratio well-posed: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Downstream code builds a concrete instance and proves the type is inhabited. Pure structure definition with no proof body.
Claim. A compression-ratio 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 compression threshold is strictly positive.
background
The module treats maximum lossless compression in the Recognition Science sense: structured data at phi-rung complexity is claimed compressible by a factor $J(\varphi)^{-1}\approx 8.47$, while random data remains incompressible (factor 1). Here $J$ is the standard RS cost $J(x)=(x+x^{-1})/2-1$, minimized at the identity $x=1$.
Domain cost is the local cost functional on model/evidence pairs used to score mismatch; the certificate demands it vanish when model equals evidence and stay nonnegative off the diagonal for positive arguments. The canonical threshold is the positive scale against which compression ratios are measured.
Upstream, nonnegativity of recognition-event cost is already forced by $J$-cost nonnegativity on positive states (ObserverForcing). This structure packages the analogous domain-level facts needed for the information-theoretic claim.
proof idea
No proof: this is a structure declaration. Its three fields are bare propositions (diagonal vanishing of domain cost, nonnegativity for positive arguments, positivity of the canonical threshold). Inhabitation is discharged later by the concrete cert instance, which plugs in the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named type for the algebraic side-conditions of the RS compression-ratio story (module status: structural theorem, zero sorry). Downstream, cert assembles a concrete certificate from the sibling lemmas, and cert_inhabited records Nonempty CompressionRatioCert, so later developments can assume a certificate without rebuilding the three facts.
In the broader framework this sits under the information layer that ties Kolmogorov-style incompressibility of random data to the forced $J$-cost and the golden-ratio fixed point $\varphi$ (T5–T6). The numerical claim $J(\varphi)^{-1}\approx 8.47$ is the intended compression factor for structured phi-rung data; the certificate does not prove that factor, only the cost/threshold hygiene needed to state it cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.