canonicalThreshold
plain-language theorem explainer
Names the real constant φ − 3/2 as the canonical threshold for RS algorithmic probability. Equals the J-cost at the golden ratio, the compression rate at which the Solomonoff prior peaks under RS-optimal encoding. Cited by anyone working the information layer of the monolith. Pure arithmetic definition in the RS constant φ; no proof burden.
Claim. The canonical threshold is the real number $\varphi - 3/2$, i.e. the value of the J-cost at the golden ratio: $J(\varphi) = \varphi - 3/2$.
background
The module treats algorithmic probability from the Recognition Science cost. Solomonoff's universal prior is $P(x) = \sum_{U(p)=x} 2^{-|p|}$. Under RS-optimal encoding the shortest program length is $J(\varphi),|x|$, so the prior peaks at the $J(\varphi)$ compression rate (module status: structural, 0 sorry, 0 axiom).
The cost is $J(x) = (x + x^{-1})/2 - 1$, the unique solution forced by the Recognition Composition Law (forcing step T5). The golden ratio $\varphi$ is the self-similar fixed point (T6). Because $\varphi^{-1} = \varphi - 1$, direct substitution yields $J(\varphi) = \varphi - 3/2$.
This definition packages that scalar for the rest of the file (positivity, domain cost comparisons, the AlgorithmicProb3Cert bundle).
proof idea
One-line definition: the real constant $\varphi - 3/2$. No tactics, no lemmas. The identification with $J(\varphi)$ is immediate from the closed form of $J$ and the minimal polynomial identity $\varphi^{-1} = \varphi - 1$; it is not re-proved here.
why it matters
Fixes the numerical compression threshold that links T5/T6 (unique J-cost and forced $\varphi$) to Solomonoff induction inside RS. Downstream siblings (threshold positivity, domain-cost comparisons, AlgorithmicProb3Cert) read this constant as the RS-optimal rate. Without a named threshold the information-layer certificates have nothing to compare against. Closes no open forcing step; it is bookkeeping that makes the structural theorem package inhabitable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.