canonicalThreshold
plain-language theorem explainer
Defines the canonical threshold as the real constant φ − 3/2. It supplies a fixed comparison scale in the J-cost monotonicity package (strict convexity of J on (0,∞), unique minimum at 1). Anyone citing domain-cost bounds or the JCostMono3 certificate would name it. The body is a bare definitional equation, not a proof.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden-ratio fixed point.
background
The ambient module develops monotonicity and convexity facts for the Recognition cost $J$. Per the module statement, $J$ is strictly convex on $(0,\infty)$, with $J'(x)=(1-x^{-2})/2$ negative below 1 and positive above, $J''(x)=x^{-3}>0$, and a unique minimum $J(1)=0$.
In the broader framework, $J$ is the unique cost forced by the Recognition Composition Law, $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The constant $\varphi$ is the self-similar fixed point from the forcing chain (T6), imported here from Constants.
The threshold $\varphi-3/2$ is a pure scale marker against which domain costs and positivity lemmas in this file are measured; it is not itself a derived inequality.
proof idea
Definitional abbreviation only: the name is bound to the real expression $\varphi - 3/2$. No tactics, no lemmas, no reduction steps.
why it matters
Sits in the Foundation J-cost monotonicity v3 package, marked structural (0 sorry, 0 axiom). It gives a named φ-native cutoff used by sibling positivity and certificate declarations (e.g. the positivity lemma for this same constant, and the JCostMono3Cert bundle). In the forcing chain it ties the cost geometry (T5 J-uniqueness) to the golden-ratio fixed point (T6), so later domain-cost comparisons stay inside RS-native units rather than ad-hoc reals. No open scaffold: the definition is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.