cert_inhabited
plain-language theorem explainer
The compression-ratio certificate type is inhabited: a concrete package of zero self-cost, nonnegative domain cost, and a positive canonical threshold exists. Anyone citing the RS Kolmogorov-limit compression bound uses this as the existence witness. The proof is a one-line term introducing the prebuilt certificate value.
Claim. The type of compression-ratio certificates is nonempty. Equivalently, there exists a record packing three facts: the domain cost vanishes on the diagonal ($\mathrm{cost}(r,r)=0$ for $r\neq 0$), the domain cost is nonnegative for positive arguments, and the canonical compression threshold is strictly positive.
background
The module treats maximum lossless compression as a Kolmogorov-style limit inside Recognition Science. Structured data at phi-rung complexity is claimed to admit an achievable compression factor $J(\varphi)^{-1}\approx 8.47$, while random data remains incompressible (factor $1$). Here $J$ is the unique cost functional forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$.
A compression-ratio certificate is a structure that packages three elementary analytic facts about the domain cost and the canonical threshold: diagonal vanishing, nonnegativity on the positive orthant, and positivity of the threshold. Those three fields are the only content of the certificate; they are the local hypotheses any later compression bound would invoke.
The certificate value itself is assembled earlier in the same module from the sibling lemmas on domain cost and the threshold.
proof idea
One-line term proof. The certificate value already constructed in-module is supplied as the witness for Nonempty, via the standard angle-bracket introduction of an existential/nonempty proof. No further rewriting or case analysis occurs.
why it matters
This is the structural existence statement for the RS compression-ratio story in the Information layer. The module presents itself as a zero-sorry structural theorem tying the Kolmogorov limit to the forced cost $J$ and the golden ratio fixed point $\varphi$ (T5–T6 of the forcing chain). Downstream consumers that need a concrete certificate object can cite this rather than re-proving the three field lemmas. No further used-by edges are recorded yet; the declaration closes the inhabitedness obligation for the certificate type itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.