cert
plain-language theorem explainer
Packages three elementary facts about the domain cost and the canonical threshold into a single AlgorithmicProb3 certificate. Anyone citing the RS link between J-cost and Solomonoff-style algorithmic probability uses this bundle. The construction is a pure record assembly of three already-proved sibling lemmas.
Claim. There exists a certificate recording that (i) the domain cost vanishes on the diagonal: $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) domain cost is nonnegative for positive arguments; and (iii) the canonical threshold is strictly positive.
background
The module treats algorithmic probability in the Recognition Science setting. The classical Solomonoff prior is $P(x)=\sum_{U(p)=x}2^{-|p|}$. Under RS-optimal encoding the shortest program length is forced to scale as $J(\varphi)\cdot|x|$, so the universal prior peaks at the $J(\varphi)$ compression rate.
Domain cost is the two-argument cost functional used here as a stand-in for program-length discrepancy between a model scale $m$ and an evidence scale $e$. The certificate structure simply demands three elementary properties of that cost and of a fixed positive threshold (the cutoff below which a program is treated as compressible).
Upstream, nonnegativity of recognition cost is already known from ObserverForcing: every recognition event has cost $\ge 0$, via nonnegativity of the J-cost on positive reals.
proof idea
One-line record construction. The three fields of the certificate structure are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No further reasoning is required.
why it matters
This is the inhabited witness that the structural hypotheses of the AlgorithmicProb3 certificate are satisfied in the J-cost model. The module is marked STRUCTURAL THEOREM (0 sorry, 0 axiom) and sits in the information layer that connects the T5 J-uniqueness cost $J(x)=(x+x^{-1})/2-1$ to Solomonoff-style algorithmic probability. Downstream consumers that need a packaged proof that domain cost is a legitimate nonnegative discrepancy with a positive compression threshold will cite this certificate (or the companion inhabitedness lemma). It does not itself derive the full Solomonoff–RS equivalence; it only discharges the cost-side side conditions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.