canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2 ≈ 0.11803, equal to the RS J-cost at the golden ratio. Structural Standard-Model arguments that treat the recognition-cost floor at φ cite this value by name. The declaration is a bare real definition, not a derived equality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio.
background
Recognition Science fixes a unique cost functional $J$ on positive reals by the Recognition Composition Law and normalization: $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). The golden ratio $\varphi$ is the self-similar fixed point forced by the T6 step of the unified forcing chain.
Because $\varphi$ satisfies $\varphi^2=\varphi+1$, one has $\varphi^{-1}=\varphi-1$, and a short algebra yields $J(\varphi)=\varphi-3/2$. The module records this numerical floor (approximately 0.11803) as the golden-ratio recognition cost and treats it as a structural constant for Standard-Model bookkeeping.
The surrounding file imports only Mathlib, the RS constants module (supplying $\varphi$), and the cost module (supplying $J$). No further hypotheses are required to name the constant.
proof idea
Pure definitional abbreviation: the real is introduced as the literal expression $\varphi-3/2$. There is no proof body, no tactic script, and no lemma application.
why it matters
The module presents the equality $J(\varphi)=\varphi-3/2$ as the structural minimum of recognition cost at the golden ratio, status STRUCTURAL THEOREM with zero sorry and zero axiom. Naming the constant lets later certificates (for example positivity of the threshold and the RS-STD structural certificate in the same file) refer to a single symbol rather than re-expanding the expression.
In the broader framework this sits at the junction of T5 (J-uniqueness) and T6 ($\varphi$ forced). Downstream Standard-Model structural claims that need a concrete positive cost floor at the self-similar point can import this definition rather than re-deriving the algebra from the closed form of $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.