cert
plain-language theorem explainer
Packages three elementary facts about domain cost and the canonical threshold into a single Kolmogorov-from-J-cost certificate. Anyone citing the structural theorem that recognition cost of encodings is governed by J will point here for the inhabited witness. The definition is a pure structure assembly: three sibling lemmas fill the three fields.
Claim. There is a 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 treats Kolmogorov complexity through Recognition Science cost. Classically $K(x)$ is the length of a shortest description of $x$. Here the recognition cost of encoding $x$ is $J(K(x)/K_{\max})$, with $J$ the unique nonnegative cost forced by the Recognition Composition Law ($J(x)=(x+x^{-1})/2-1$). Incompressible strings sit at $J=0$ (all descriptions equally costly); regular strings sit at $J(\varphi)$.
domainCost is the local cost functional on pairs of positive reals used as the encoding cost model. The certificate structure KolmogComplx3Cert records three structural properties that any such model must satisfy before one can speak of a complexity threshold: vanishing on the diagonal, nonnegativity off the axes, and a positive cutoff.
Upstream, nonnegativity of recognition-event cost is already known from ObserverForcing (cost_nonneg: every recognition event has nonnegative $J$-cost).
proof idea
One-line structure construction. The three fields are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the cutoff). No further rewriting or case analysis.
why it matters
This is the inhabited witness for the module's structural theorem (status: 0 sorry, 0 axiom) linking Kolmogorov complexity to $J$-cost. Downstream consumers that need a KolmogComplx3Cert value (for example the sibling cert_inhabited) obtain it here rather than re-proving the three field obligations. In the broader RS chain it sits on the information side of the forcing story: once $J$ is unique (T5) and $\varphi$ is fixed (T6), encoding cost and compressibility thresholds become well-defined numerical objects. No open scaffold remains in this module; the certificate is fully discharged.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.