canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold constant of the J-cost algorithmic-probability module is strictly positive. Anyone building or citing the RS Solomonoff-style prior peak, domain-cost nonnegativity, or the AlgorithmicProb3 certificate needs this sign fact. The proof is a one-line wrapper: unfold the threshold and close by linear arithmetic from φ > 1.5.
Claim. The canonical threshold $T$ of the algorithmic-probability-from-$J$-cost module satisfies $0 < T$.
background
This module sits in the Information layer and treats algorithmic (Solomonoff) probability as a consequence of RS $J$-cost. The module doc states the structural claim: at an RS-optimal encoding the shortest program length scales as $J(\varphi),|x|$, so the universal prior $P(x)=\sum_{U(p)=x}2^{-|p|}$ peaks at the $J(\varphi)$ compression rate. Status is structural (0 sorry, 0 axiom).
The cost functional is the unique $J$ forced by the Recognition Composition Law and T5, $J(x)=(x+x^{-1})/2-1$. The golden ratio $\varphi=(1+\sqrt{5})/2$ is the self-similar fixed point (T6) and sets the native compression scale. Upstream, phi_gt_onePointFive records the elementary bound $\varphi>1.5$ (from $\sqrt{5}>2$).
The canonical threshold is the real constant built from $\varphi$ that this module uses as a positivity gate for later certificate constructions (domain cost and AlgorithmicProb3).
proof idea
One-line wrapper. Unfold the definition of the canonical threshold, then discharge the resulting arithmetic inequality by linarith using the upstream lemma $\varphi>1.5$. No case splits, no induction, no further RS lemmas.
why it matters
Positivity of the threshold is the elementary sign fact that keeps the algorithmic-probability certificate well-defined: a non-positive threshold would collapse the claimed peak of the universal prior at the $J(\varphi)$ rate. The module is marked structural theorem (0 sorry). Downstream siblings in the same file (domain-cost nonnegativity, AlgorithmicProb3Cert, cert inhabited) are the natural consumers, even though the rendered used-by list is still empty.
Framework landmarks: T5 $J$-uniqueness and T6 $\varphi$-forcing fix the compression scale; the eight-tick and $D=3$ steps are not used here. The result does not itself derive the Solomonoff formula; it only clears the positivity gate for that derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.