canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold equals the golden-ratio cost J(φ)=φ−3/2 and is strictly positive. Structural theorems that quote the RS cost floor at φ cite this fact. The proof unfolds the definition and finishes by linear arithmetic from the elementary bound φ>3/2.
Claim. The canonical threshold $J(\varphi)=\varphi-\tfrac{3}{2}$ is strictly positive: $0<J(\varphi)$, where $\varphi=(1+\sqrt{5})/2$ is the golden ratio.
background
Recognition Science forces a unique cost functional $J$ via the Recognition Composition Law, with closed form $J(x)=(x+x^{-1})/2-1$. At the self-similar fixed point $\varphi$ (forcing step T6) one obtains the golden-ratio recognition cost $J(\varphi)=\varphi-3/2\approx 0.118$.
This module records that structural minimum as a named real constant (the canonical threshold) together with elementary evaluation and sign lemmas. The setting is pure real analysis over the RS constants imported from Constants and Cost; no units or physical interpretation are attached here.
The only upstream lemma required is the tighter lower bound $\varphi>1.5$, which follows at once from $\sqrt{5}>2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (equal to $\varphi-3/2$), then apply linarith to the hypothesis $\varphi>1.5$ supplied by phi_gt_onePointFive.
why it matters
Positivity of $J(\varphi)$ is the elementary sign fact behind the claim that the golden-ratio rung carries a strictly positive recognition cost, the structural minimum quoted in the module header. The file marks the result STRUCTURAL THEOREM (zero sorry, zero axiom). Sibling certificate constructors in the same module package the inequality for export; no external downstream edges are recorded yet. The lemma sits under the T5–T6 segment of the forcing chain (J-uniqueness and $\varphi$ as fixed point) and underwrites the numerical floor $0.118$ used when comparing ladder costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.