canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2, with φ the golden ratio. It supplies a fixed comparison level for domain costs in the J-cost symmetry module of the RS forcing chain. Anyone citing Module 9 structural results on ratio-symmetric recognition cost would use it. The declaration is a one-line definitional assignment, not a proved claim.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden ratio.
background
Foundation Module 9 treats RS J-cost symmetry: recognition cost is ratio-symmetric, i.e. $J(x)=J(1/x)$. Status is structural (zero sorry, zero axiom). The cost $J$ is the unique functional forced at T5, $J(x)=(x+x^{-1})/2-1$, also written $\cosh(\log x)-1$, and obeying the Recognition Composition Law.
Constants are drawn from the RS constants module; $\varphi$ is the self-similar fixed point forced at T6. Domain costs in this module are real-valued quantities built from $J$ and compared against a fixed numerical level. The present declaration names that level as $\varphi-3/2$.
proof idea
Definitional only: the real is set equal to $\varphi-3/2$. No tactics, no lemmas, no proof obligations.
why it matters
Gives the numerical anchor used by sibling positivity and certificate results in the same module (e.g. positivity of the threshold and the Module 9 forcing-chain certificate). Sits inside the structural half of the forcing chain: T5 uniqueness of $J$, T6 forcing of $\varphi$, and the ratio symmetry $J(x)=J(1/x)$ that Module 9 records. It is not itself a chain step T0–T8, but a local constant those structural theorems compare against when bounding domain cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.