canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold as $\varphi - 3/2$, where $\varphi$ is the RS self-similar fixed point. Structural certificates and domain-cost comparisons in the T5–T8 forcing chain cite this constant as the cut separating admissible from inadmissible cost regimes. The body is a one-line arithmetic definition.
Claim. The canonical threshold is the real number $\varphi - 3/2$, with $\varphi$ the unique self-similar fixed point forced by the Recognition Composition Law (T6).
background
Module RS_MTH_Structural_009 sits in the mathematics layer of the RS forcing chain: T5 uniqueness of the J-cost $J(x)=(x+x^{-1})/2-1$, T6 forcing of $\varphi$ as the self-similar fixed point, T7 the eight-tick octave, and T8 spatial dimension $D=3$. Status is structural (zero sorry, zero axiom).
$\varphi$ is imported from the Constants layer and is the unique positive solution of the fixed-point relation that makes the cost self-similar under the Recognition Composition Law. The sibling domainCost packages a non-negative cost functional on a domain; the threshold is the natural comparison value against which that cost is tested.
No upstream lemmas are required: the definition is pure arithmetic in the reals once $\varphi$ is in scope.
proof idea
Pure definitional abbreviation. The right-hand side is the real expression $\varphi - 3/2$; no tactics, no lemmas, no rewriting.
why it matters
Gives a single named cut in the cost line that later positivity and certificate lemmas (e.g. the sibling positivity statement and the structural certificate RSMTHStructural009Cert) can quote without re-deriving $\varphi-3/2$. In the forcing chain it sits after T6 ($\varphi$ forced) and supplies a concrete numerical gate for domain-cost admissibility arguments that feed the eight-tick and $D=3$ steps. It does not itself prove uniqueness or positivity; those are separate sibling claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.