cert
plain-language theorem explainer
Packages three domain-cost facts into one Kolmogorov certificate: diagonal vanishing, nonnegativity for positive mass and energy, and a positive canonical threshold. Cited by anyone working with RS Kolmogorov complexity as the standing witness that the cost model is well-posed. Proof is a structure instance wiring three already-proved sibling lemmas.
Claim. There is a Kolmogorov certificate consisting of: (i) $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module develops Recognition Science Kolmogorov complexity: $K_{\mathrm{RS}}(x)=\log_\phi(|x|)\cdot J(\phi)^{-1}$, so recognition complexity grows as a $\phi$-base logarithm of data length (numerically $\approx 8.47,\log_\phi(|x|)$). Status is structural: zero sorry, zero axiom.
KolmogorovCert is the structure that packages the three well-posedness obligations for the domain cost used in that story: the cost vanishes when mass equals energy on the diagonal (away from zero), stays nonnegative for positive arguments, and the canonical threshold used as a cutoff is positive.
Upstream, nonnegativity of recognition cost is already forced in ObserverForcing: "The cost of any recognition event is non-negative," via $J$-cost nonnegativity. The present certificate lifts the analogous facts to the information-theoretic domain cost.
proof idea
One-line structure instance. The three fields of KolmogorovCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No extra algebra or tactics; the definition is pure assembly of prior proofs.
why it matters
Gives a single named witness that the RS domain-cost model for Kolmogorov complexity is coherent: zero on matched arguments, nonnegative off-diagonal, and cut off by a positive threshold. That is the structural prerequisite for treating $K_{\mathrm{RS}}$ as a genuine complexity measure on the $\phi$-ladder rather than an ad hoc formula.
No downstream consumers are recorded yet in the graph; the immediate sibling cert_inhabited is the natural next step (nonemptiness of the certificate type). In the broader framework this sits in the information layer that rides on the $J$-cost uniqueness (T5) and the $\phi$ fixed point (T6), without itself advancing the forcing chain T0–T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.