canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2, the J-cost of the golden ratio. Foundation work cites it as the equilibrium cost level at the self-similar fixed point of the Recognition Composition Law. It is a one-line arithmetic definition in the RS constant φ, not a proved identity.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden ratio.
background
Module 4 of the RS forcing chain records the elementary geometry of the J-cost on the positive reals. The cost is $J(x) = (x + x^{-1})/2 - 1$ (equivalently $\cosh(\log x) - 1$). It vanishes only at ratio one: $J(1) = 0$, the equilibrium of the Recognition Composition Law.
The golden ratio $\varphi$ is the unique self-similar fixed point forced by T6. Direct substitution yields $J(\varphi) = \varphi - 3/2$. The present definition simply names that real number so later lemmas can refer to a single constant rather than the expanded expression.
The module imports the global RS constants (including $\varphi$) and the Cost layer that supplies $J$. Status is structural: zero sorry, zero axioms.
proof idea
Pure definitional abbreviation. The body is the arithmetic term $\varphi - 3/2$ with no proof obligations, no tactics, and no upstream lemmas.
why it matters
Names the numerical value of $J$ at the T6 fixed point, the cost level that later positivity and comparison lemmas treat as the canonical threshold. Sits inside the structural core of the forcing chain (T5 J-uniqueness, T6 $\varphi$-forcing) and supplies the constant used by sibling facts such as positivity of the threshold. Downstream certificates in the same module package the threshold together with non-negativity of domain cost, keeping the J-minimum story self-contained.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.