canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2, with φ the golden ratio fixed by self-similarity. It is the cutoff used when comparing domain costs in the structural module that encodes the RS count law 2^D − 1 = 7 at D = 3. Anyone normalizing recognition costs against a fixed positive scale would cite it. The declaration is a one-line definitional binding with no proof obligations.
Claim. Define the canonical threshold as the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio.
background
This module is Foundation structural module 3. Its stated content is the RS count law: with spatial dimension $D = 3$ one has $2^D - 1 = 7$ independent channels, recorded as a structural theorem with no sorry and no extra axioms.
The constant $\varphi$ is imported from the RS constants layer (T6: the unique self-similar fixed point of the recognition scaling). The Cost import supplies the domain-cost primitives against which a fixed real cutoff is compared; sibling facts in the file assert nonnegativity of that cost and positivity of this threshold.
In the broader forcing chain, $D = 3$ is the T8 landmark; the eight-tick octave and the J-cost $J(x) = (x + x^{-1})/2 - 1$ sit upstream of the count-law bookkeeping this module packages.
proof idea
Definitional. The name is bound directly to the real expression $\varphi - 3/2$. There is no tactic proof, no lemma application, and no hypothesis to discharge.
why it matters
Gives a single named real scale for cost comparisons inside the D = 3 count-law module (seven independent channels). Sibling positivity of the threshold and the module certificate inhabit the same file, so the constant is the numeric anchor those facts refer to.
In the Recognition framework it sits next to the T6 forcing of $\varphi$ and the T8 forcing of three spatial dimensions. It is not the Berry creation threshold $\varphi^{-1}$; it is a separate structural cutoff of the form $\varphi - 3/2$. No downstream edges are recorded on this page, so its role is local to the structural certificate rather than a named parent theorem elsewhere.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.