AlgorithmicProb3Cert
plain-language theorem explainer
A certificate bundling three arithmetic facts that link domain cost to algorithmic (Solomonoff) probability: diagonal cost vanishes, cost is nonnegative on the positive quadrant, and the canonical compression threshold is positive. Cited by anyone deriving the RS claim that the universal prior peaks at the J(φ) rate. Pure structure definition; inhabitance is assembled later from sibling lemmas.
Claim. A certificate is a triple of properties of the domain cost $C$ and canonical threshold $\tau$: (i) $C(r,r)=0$ for every $r\neq 0$; (ii) $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) $\tau>0$.
background
The module treats algorithmic probability as a consequence of Recognition Science J-cost. Classically the Solomonoff prior is $P(x)=\sum_{p:U(p)=x}2^{-|p|}$. RS asserts that at an RS-optimal encoding the shortest program length equals $J(\varphi)\cdot|x|$, so the universal prior concentrates at the $J(\varphi)$ compression rate.
Domain cost is the local cost on pairs of positive reals (model and evidence scales), built from the J-cost $J(x)=(x+x^{-1})/2-1$. The canonical threshold is the positive cutoff that marks when compression beats the bare prior. Upstream, ObserverForcing already records that every recognition-event cost is nonnegative, via nonnegativity of J-cost on positive states.
proof idea
No proof body: this is a structure declaration whose three fields are Prop-valued requirements. Downstream, the concrete instance fills them by the sibling facts that domain cost vanishes on the diagonal, is nonnegative for positive arguments, and that the canonical threshold is positive. Inhabitance is then a one-constructor witness packaging that instance.
why it matters
This certificate is the interface satisfied by the module's concrete instance and its inhabitance theorem. It packages exactly the cost identities needed so a Solomonoff-style sum is dominated by programs whose length tracks $J(\varphi)|x|$. It underwrites the module's structural claim (zero sorry, zero axiom) that algorithmic probability emerges from J-cost.
Framework landmarks: T5 forces the J-shape used by domain cost; T6 forces $\varphi$ as the self-similar fixed point that sets the compression rate. Downstream consumers only need the bundled triple, not the internal construction of domain cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.