canonicalThreshold_pos
plain-language theorem explainer
The canonical threshold equals J(φ)=φ−3/2 and is strictly positive. Anyone using the RS dimensionless identity at the golden ratio, or needing a positivity gate on that cost, would cite this. Proof is a one-line unfold plus linear arithmetic from the bound φ>1.5.
Claim. The canonical threshold, defined as $\varphi-3/2$ (equivalently $J(\varphi)$), is strictly positive: $0<\varphi-3/2$.
background
Recognition Science forces a unique cost $J(x)=(x+x^{-1})/2-1$ (T5). At the golden ratio $\varphi=(1+\sqrt{5})/2$, the exact evaluation is $J(\varphi)=\varphi-3/2\approx 0.11803$. Module 12 records that dimensionless identity as a structural theorem (zero sorry, zero axioms).
The canonical threshold is that value $\varphi-3/2$. The only upstream fact needed here is the elementary bound $\varphi>1.5$, which follows from $\sqrt{5}>2$ and is already proved in Constants.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (so the goal becomes $0<\varphi-3/2$), then finish by linarith using the lemma $\varphi>1.5$.
why it matters
Positivity of $J(\varphi)$ is the elementary gate that the self-similar fixed point sits strictly above zero cost. It sits after T5 (J-uniqueness) and T6 ($\varphi$ forced) in the forcing chain, and underwrites the module's claim that $J(\varphi)=\varphi-3/2$ exactly. No downstream dependents are recorded in this slice; the lemma is available to any certificate that needs a positive dimensionless cost at $\varphi$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.