canonicalThreshold
plain-language theorem explainer
Names the exact real value φ − 3/2 as the canonical cost threshold. Anyone citing the closed form of the J-cost at the golden ratio uses this constant. It is a one-line definition equal to the algebraic simplification of J(φ).
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio.
background
Recognition Science fixes the cost functional $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$) by the T5 uniqueness step of the forcing chain. The golden ratio $\varphi$ is forced as the self-similar fixed point (T6).
Direct substitution yields $J(\varphi) = (\varphi + \varphi^{-1})/2 - 1$. Using $\varphi^{-1} = \varphi - 1$ this collapses to $\varphi - 3/2$. The module records that identity as an exact structural fact: $J(\varphi) = \varphi - 3/2 \approx 0.118$.
This definition simply packages that real number under a stable name for later certificates and inequalities in the same file (non-negativity of domain cost, exactness certificates).
proof idea
Pure definition: the right-hand side is the arithmetic expression $\varphi - 3/2$ in the reals, with $\varphi$ imported from the Constants module. No proof obligations.
why it matters
Gives a named constant for the exact value of the J-cost at $\varphi$, which the module treats as a structural theorem of the foundation layer. Downstream siblings (exactness certificates, positivity of the threshold) compare domain costs against this number. It sits at the T5–T6 junction: once $J$ and $\varphi$ are forced, their evaluation is no longer free. The numerical size $\approx 0.118$ is the concrete scale against which recognition defects are measured in RS-native units.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.