domainCost_nonneg
plain-language theorem explainer
Domain cost is nonnegative whenever mass and energy parameters are positive. Information-theoretic arguments that bound Solomonoff-style priors by J-cost cite this elementary positivity fact. The proof is a one-line unfold of the domain-cost definition followed by the standard nonnegativity lemma for J on the positive ratio m/e.
Claim. For all real numbers $m>0$ and $e>0$, the domain cost satisfies $0\le C_{\mathrm{dom}}(m,e)$. (Here domain cost is the J-cost of the positive ratio $m/e$.)
background
The ambient module derives algorithmic-probability structure from Recognition Science J-cost. The Solomonoff prior $P(x)=\sum_{U(p)=x}2^{-|p|}$ is compared, at RS-optimal encoding, to a compression rate set by $J(\varphi)$: shortest programs scale as $J(\varphi)\cdot|x|$, so the universal prior peaks at that rate.
J-cost is the unique nonnegative cost forced by the Recognition Composition Law: $J(x)=(x+x^{-1})/2-1$ for $x>0$ (equivalently $\cosh(\log x)-1$). Upstream lemmas record $J(x)\ge 0$ for every positive $x$, proved by rewriting as a square over a positive denominator (AM-GM).
Domain cost is the specialization of that cost to a positive mass/energy ratio: after unfolding, $C_{\mathrm{dom}}(m,e)=J(m/e)$. The present statement simply transports J-nonnegativity to that pair of parameters.
proof idea
One-line wrapper. Unfold the definition of domain cost so the goal becomes nonnegativity of $J(m/e)$. The hypotheses $m>0$ and $e>0$ give $m/e>0$ by div_pos. Apply the upstream lemma Jcost_nonneg to that positive ratio and finish.
why it matters
Sits in the structural (zero-sorry) development that links Solomonoff algorithmic probability to RS J-cost. Nonnegativity is the first arithmetic hygiene fact needed before thresholds, certificates, or comparison inequalities involving domain cost can be stated. It inherits the T5 uniqueness of $J$ and the AM-GM identity $J(x)=(x-1)^2/(2x)$. No downstream consumers are recorded yet; the sibling cluster (canonical threshold positivity, AlgorithmicProb3 certificate) is the natural landing zone once those objects quantify over domain cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.