canonicalThreshold
plain-language theorem explainer
Defines the canonical numerical threshold as the golden ratio minus 3/2. Structural RS mathematics cites it when comparing domain costs or positivity bounds against a fixed real cutoff. The body is a one-line definitional abbreviation from Constants.phi.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden ratio.
background
Module RS_MTH_Structural_001 packages structural RS predictions: the unique cost $J(x)=\frac12(x+1/x)-1$, the golden ratio $\varphi$ as the self-similar fixed point, and the forcing of spatial dimension $D=3$. Status is a structural theorem block with zero sorry and zero axioms.
The constant $\varphi$ is imported from IndisputableMonolith.Constants (T6 in the forcing chain). The Cost import supplies the $J$-cost used by sibling definitions such as domainCost. The threshold $\varphi-3/2$ sits slightly above $0.118$ and is the fixed real scale against which those domain costs are compared in this module.
proof idea
Pure definition: the name is bound to the real expression $\varphi - 3/2$. No tactics, no lemmas, no proof obligations.
why it matters
Gives a single named real cutoff for the structural mathematics certificate in this module (siblings include canonicalThreshold_pos and RSMTHStructural001Cert). It sits downstream of T5–T6 ($J$-uniqueness and $\varphi$ forced) and supplies the comparison scale used when the module asserts nonnegativity or structural bounds on domain costs. Not itself a forcing step; it is the concrete number those structural claims measure against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.