canonicalThreshold_pos
plain-language theorem explainer
The canonical recognition threshold equals J(φ)=φ−3/2 and is strictly positive. Cosmology and RS cost-structure arguments cite it whenever the golden-ratio minimum cost must sit above zero. Proof is a one-line unfold of the threshold definition followed by linear arithmetic from the bound φ>1.5.
Claim. The canonical threshold $J(\varphi)=\varphi-\tfrac{3}{2}$ satisfies $0<J(\varphi)$, where $\varphi=(1+\sqrt{5})/2$ is the golden ratio.
background
Recognition Science measures mismatch by the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $\cosh(\log x)-1$. On the positive reals this cost is minimized uniquely at the golden ratio $\varphi$, and the minimum value collapses algebraically to $J(\varphi)=\varphi-3/2\approx 0.118$.
This module packages that minimum as a named structural constant (the canonical threshold) for cosmology-side arguments. The only upstream fact needed here is the elementary bound $\varphi>1.5$, recorded as a tighter lower estimate from $\sqrt{5}>2$.
proof idea
One-line wrapper. Unfold the definition of the canonical threshold (so the goal becomes $0<\varphi-3/2$), then discharge by linarith using the lemma $\varphi>1.5$. No further cost identities are required.
why it matters
Places the golden-ratio recognition cost strictly above zero inside the cosmology structural layer (RS Structural Module 2). That positivity is the quantitative content of the claim "J-cost minimum at φ equals φ−3/2≈0.118". It sits downstream of the T5/T6 forcing facts that single out J and φ, and it supplies a concrete positive scale for any later cosmology certificate that compares domain costs against the φ-minimum. No downstream consumers are wired yet in this graph snapshot; the lemma is infrastructure for those certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.