canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2, with φ the golden-ratio fixed point of Recognition Science. Module-5 forcing-chain material cites it as a fixed positive cutoff against which domain costs are compared. The declaration is a one-line arithmetic definition, not a derived inequality.
Claim. Define the canonical threshold by $\mathrm{canonicalThreshold} := \varphi - \tfrac{3}{2}\in\mathbb{R}$, where $\varphi$ is the unique positive self-similar fixed point of the Recognition cost (the golden ratio).
background
Module 5 of the RS forcing chain records structural theorems for T0–T8 with zero sorry and zero extra axioms. The chain forces the cost functional $J$, then $\varphi$ as its self-similar fixed point (T5–T6), the eight-tick octave, and $D=3$.
Here $\varphi$ is imported from the Constants layer; numerically $\varphi=(1+\sqrt{5})/2\approx 1.618$, so $\varphi-3/2\approx 0.118$. Sibling definitions in the same file introduce a domain cost built from the Recognition $J$-cost and compare it to this threshold. The Cost import supplies the underlying nonnegative cost geometry against which thresholds are meaningful.
proof idea
Pure definition: the name is bound to the real expression $\varphi-3/2$. No tactic proof, no lemmas, no reduction. Positivity and comparison lemmas live in sibling declarations (for example the positivity certificate for the same constant).
why it matters
Gives a single named real cutoff used by the module-5 certificate bundle for the RS forcing chain. In the broader framework it sits downstream of T6 ($\varphi$ forced) and upstream of any comparison that asks whether a domain cost clears a fixed positive bar. The module status line marks the surrounding development as a structural theorem block (0 sorry). This definition itself does not close a chain step; it standardizes the numerical gate those steps reference.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.