canonicalThreshold
plain-language theorem explainer
Defines the canonical numerical threshold as φ − 3/2 in RS units. Eight-tick application arguments cite it as the fixed comparison level against domain costs. The body is a one-line real definition, not a derived equality.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the RS self-similar fixed point (golden ratio).
background
The module collects structural 8-tick applications: musical octave, color×flavor quark count, SU(3) gluons, Gell-Mann eightfold way, and related 2^D = 8 patterns with D = 3. Status is a structural theorem layer (no sorry, no axioms).
φ is the unique self-similar fixed point forced in the Recognition chain (T6). It is imported from Constants and used throughout Cost and foundation modules. Domain costs in this file are non-negative real functionals compared against a single fixed level; that level is named here.
No upstream lemma is required: the declaration only names the combination φ − 3/2.
proof idea
Bare definition. The right-hand side is the real expression φ − 3/2; there is no tactic proof, no lemma application, and no reduction.
why it matters
Gives a single named constant for threshold comparisons inside the eight-tick applications layer. The module ties those applications to the forced period 2^3 (T7) and spatial D = 3 (T8). Sibling positivity (canonicalThreshold_pos) and domain-cost lemmas sit next to it; the definition itself is the shared numeric anchor rather than a forcing step.
It does not appear in the T0–T8 chain or the RCL identity; it is local scaffolding for the v2 applications certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.