canonicalThreshold
plain-language theorem explainer
Defines the canonical structural threshold as φ − 3/2 in RS-native units. Foundation and cost-module arguments cite it as the fixed real cutoff against which domain costs are compared. The body is a one-line constant abbreviation from the golden ratio.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the unique self-similar fixed point forced by the Recognition composition law.
background
Module RS_FDN_Structural_009 sits on the RS forcing chain after T5–T6: the cost functional $J$ is unique, and $\varphi$ is forced as the self-similar fixed point of the composition law $J(xy)+J(x/y)=2J(x)J(y)+2J(x)+2J(y)$. Imports pull $\varphi$ from Constants and the cost layer from Cost.
Sibling definitions introduce a nonnegative domain cost and compare it to this threshold. The module is marked structural (zero sorry, zero axiom) and records the chain T5 $\varphi$-uniqueness through T8 ($D=3$).
proof idea
Pure definition: the real constant is written as $\varphi - 3/2$. No proof obligations; positivity and comparisons are discharged by sibling lemmas such as the positivity certificate for the same constant.
why it matters
Gives a single named real cutoff for structural comparisons in the foundation layer, so domain-cost inequalities and the module certificate can refer to one symbol rather than an inline expression. It sits downstream of T6 ($\varphi$ forced) and upstream of the structural certificate bundle in this file. Numerically $\varphi-3/2\approx 0.118$, distinct from the Berry creation scale $\varphi^{-1}$ and from the dream fraction $\varphi^{-3}$; it is a bookkeeping threshold for cost comparisons, not a mass or coupling constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.