canonicalThreshold
plain-language theorem explainer
Defines the canonical recognition threshold as φ − 3/2, which equals J(φ) for the RS cost J(x)=(x+1/x)/2−1. Anyone citing the Logo5 cost curve or domain-cost positivity uses this constant as the natural height of the curve at the golden fixed point. The body is a one-line real definition from Constants.phi.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio. Equivalently, it is the value $J(\varphi)$ of the recognition cost $J(x)=(x+x^{-1})/2-1$ at $x=\varphi$.
background
Recognition Science Logo5 treats the single curve $J(x)=(x+1/x)/2-1$ on $(0,\infty)$ as the entire cost geometry of the theory. $J$ has a unique minimum $J(1)=0$ and is forced (T5) by the Recognition Composition Law; $\varphi$ is the self-similar fixed point (T6).
Because $\varphi$ satisfies $\varphi=1+1/\varphi$, one has $J(\varphi)=\varphi-3/2$. The module therefore names this height canonicalThreshold: the cost value attained when the argument sits at the golden ratio. Sibling lemmas record nonnegativity of a domain cost built from $J$ and positivity of this threshold.
Imports are Mathlib, Constants (for $\varphi$), and Cost (for $J$). No upstream theorems are required; the equality $J(\varphi)=\varphi-3/2$ is pure algebra from the golden equation.
proof idea
Pure definition: the real constant is introduced as $\varphi-3/2$ with no proof obligations. The identification with $J(\varphi)$ is the one-line expansion $J(\varphi)=(\varphi+\varphi^{-1})/2-1$ together with $\varphi^{-1}=\varphi-1$.
why it matters
Gives the absolute vertical scale of the RS logo curve at the golden point. Module status is structural (0 sorry, 0 axiom): one curve, all of physics. Downstream siblings such as positivity of the threshold and the Logo5 certificate package treat this constant as the reference height against which domain costs are compared.
In the forcing chain it sits at the junction of T5 (J-uniqueness) and T6 ($\varphi$ forced). It is the natural companion to the Berry creation threshold $\varphi^{-1}$ on the horizontal axis: here the vertical cost coordinate at $x=\varphi$ is fixed once and for all.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.