canonicalThreshold
plain-language theorem explainer
Defines the real scalar φ − 3/2 as the canonical threshold used in the RS Tribonacci module. Anyone comparing domain costs or certifying the Tribonacci fixed-point structure at D = 3 cites this constant. It is a pure abbreviation of the golden-ratio offset; no proof is required.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio fixed by the self-similarity equation of Recognition Science.
background
The module treats the Tribonacci constant $T\approx 1.839$ (root of $T^3=T^2+T+1$) as the structural growth rate of a three-term recognition chain at spatial dimension $D=3$. In RS the golden ratio $\varphi$ is forced as the unique self-similar fixed point (forcing step T6); the eight-tick octave and $D=3$ follow at T7–T8.
Sibling definitions introduce a non-negative domain cost on the real line and a certificate package TribonacciCert. The present constant supplies the numerical cut that those objects compare against. Imports pull $\varphi$ from Constants and the J-cost infrastructure from Cost, but the definition itself only needs $\varphi$.
proof idea
Pure definitional abbreviation: the real expression $\varphi-3/2$ is bound to the name. No tactics, lemmas, or rewriting are involved.
why it matters
Gives a single named scalar for every positivity or comparison lemma in the Tribonacci RS layer (e.g. canonicalThreshold_pos and the inhabited certificate). The module frames the construction as a structural theorem with zero sorry and zero axioms, tying the three-term recurrence to the forced dimension $D=3$. The numerical offset $\varphi-3/2\approx 0.118$ sits well below the Berry creation scale $\varphi^{-1}$ and is therefore a mild, RS-native threshold rather than an independent physical constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.