canonicalThreshold
plain-language theorem explainer
The golden-ratio recognition cost is the real constant φ − 3/2 ≈ 0.118. Cosmology and RS cost arguments cite it as the J-cost minimum at the self-similar fixed point. The declaration is a one-line definition fixing that closed form.
Claim. The canonical recognition threshold is the real number $\varphi - 3/2$, equal to the J-cost of the golden ratio: $J(\varphi) = \varphi - 3/2$.
background
Recognition Science fixes a unique nonnegative cost $J$ on the positive reals by the Recognition Composition Law and normalization. Explicitly, $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 same chain (T5–T6).
Because $\varphi$ satisfies $\varphi = 1 + 1/\varphi$, a short algebra yields $J(\varphi) = \varphi - 3/2 \approx 0.11803$. This module packages that value as the structural constant for cosmology-facing cost comparisons.
Local setting (module doc): RS J-cost minimum at $\varphi$, recorded as a structural theorem with no sorry and no extra axioms. Sibling facts establish nonnegativity of a domain cost and positivity of this threshold.
proof idea
Pure definition: the constant is introduced by the equality $\texttt{canonicalThreshold} := \varphi - 3/2$. No lemma application or tactic proof is required; downstream positivity and cost identities refer to this name.
why it matters
Gives cosmology code a single named real for the golden-ratio recognition cost, matching the module claim $J(\varphi) = \varphi - 3/2$. It sits on the forcing chain landmarks T5 (J-uniqueness) and T6 ($\varphi$ as self-similar fixed point). Sibling lemmas (threshold positivity, domain-cost nonnegativity, the structural certificate) build on this constant so that later cosmology comparisons can quote one closed form rather than re-deriving the algebra each time.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.