canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold as φ − 3/2, with φ the golden-ratio fixed point of the Recognition cost. Summary and certificate modules cite it when comparing domain costs or positivity bounds against a single fixed cutoff. The body is a one-line arithmetic definition, not a derived inequality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the unique self-similar fixed point forced by the Recognition cost $J$.
background
Recognition Science forces a unique cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$) from four axioms, then forces $\varphi$ as the self-similar fixed point of that cost (forcing chain T5–T6). Constants live in RS-native units with $c=1$ and powers of $\varphi$ setting $\hbar$ and $G$.
This module is the Plan v7 structural summary certificate: zero sorry, zero axioms, packaging that $J$ uniqueness implies $\varphi$, gap-45, $D=3$, and the derived constants. The threshold sits beside domain-cost helpers that evaluate $J$ on positive reals and prove nonnegativity, so comparisons need a single named cutoff built from $\varphi$.
proof idea
Pure definition: the real constant is introduced as the arithmetic expression $\varphi - 3/2$. No lemmas, tactics, or proof obligations; positivity and uses appear in sibling declarations.
why it matters
Gives the summary certificate a single named real cutoff built from the forced scale $\varphi$, rather than an ad-hoc decimal. Downstream siblings (positivity of the threshold, domain-cost comparisons, and the inhabited RS summary certificate) can quote one symbol instead of repeating $\varphi-3/2$. It is not itself a forcing-chain step (T0–T8), but it packages the $\varphi$ landmark for certificate-level bounds in the Foundation layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.