canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2, with φ the golden-ratio fixed point of the forcing chain. It is the comparison level used when domain costs are measured against a fixed positive cutoff in the T0–T8 completeness development. Anyone citing threshold positivity or domain-cost inequalities in this module refers to this value. The declaration is a one-line definitional abbreviation.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden ratio (self-similar fixed point of the Recognition forcing chain).
background
The module completes the T0–T8 forcing chain: all physical constants are derived from the unique J-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$). Along that chain, T3/T6 force $\varphi$ as the self-similar fixed point of the Recognition Composition Law, and later steps recover the eight-tick period, $D=3$, and the fine-structure band.
Sibling material in the same file introduces a nonnegative domain cost built from $J$ and compares it to a fixed real cutoff. The cutoff used for those comparisons is this canonical threshold. Imports supply $\varphi$ from Constants and the cost functional from Cost; no further hypotheses are attached to the definition itself.
proof idea
Pure definition: the real constant is introduced by the single equation $\texttt{canonicalThreshold} := \varphi - 3/2$. There is no proof body, tactic block, or lemma application.
why it matters
Inside ForcingChainCompleteness3 the threshold supplies the numerical level against which domain costs are tested (siblings include positivity of the threshold and the structural certificate ForcingChainComp3Cert). It sits in the same layer as the J-uniqueness and $\varphi$-forcing steps of the primer chain (T5–T6), giving a concrete positive scale once $\varphi$ is fixed. The value is not itself a physical constant of the RS unit system; it is an auxiliary cutoff that lets the completeness certificate speak uniformly about cost gaps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.