canonicalThreshold
plain-language theorem explainer
Defines the canonical threshold as $\varphi - 3/2$ in RS-native reals. Standard-model structural arguments that compare domain cost against a fixed positive cutoff cite this constant. The body is a one-line abbreviation of that difference; positivity is left to a sibling lemma.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the self-similar fixed point of $x \mapsto 1 + 1/x$ (the golden ratio forced by the Recognition chain).
background
Module RS_STD_Structural_006 packages structural facts about $\varphi$-uniqueness in the Standard Model layer: $\varphi = 1 + 1/(1+1/(1+\cdots))$ is the unique self-similar fixed point (forcing landmark T6). The module imports Constants (for $\varphi$) and Cost (for the J-cost and related domain-cost machinery).
Sibling declarations introduce a domain cost functional and prove it is nonnegative. The present definition supplies the numerical cutoff against which that cost is compared. Numerically $\varphi \approx 1.618$, so the threshold is a small positive real near $0.118$.
proof idea
Pure definition: the real constant is introduced by the equation $\mathrm{canonicalThreshold} := \varphi - 3/2$. No tactics or lemmas are involved. Downstream positivity and certificate packing live in sibling declarations (canonicalThreshold_pos, RSSTDStructural006Cert).
why it matters
Gives a single named cutoff for structural Standard Model certificates that sit on the $\varphi$-uniqueness story (module status: structural theorem, zero sorry, zero axiom). Ties directly to T6 in the forcing chain: once $\varphi$ is forced as the self-similar fixed point, differences such as $\varphi - 3/2$ become canonical scales for cost comparisons. Feeds the module certificate (RSSTDStructural006Cert / cert) that packages the structural claims for this file. No open scaffold: the definition is closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.