canonicalThreshold
plain-language theorem explainer
Defines the canonical gravity threshold as the golden ratio minus 3/2. Gravity and RS structural work cites it as the fixed numerical cutoff tied to phi-ladder rung spacing. The body is a one-line real constant, not a proof.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden ratio (self-similar fixed point of the Recognition forcing chain).
background
Module 8 of the RS gravity structural series fixes rung spacing: adjacent rungs differ by the factor $\varphi \approx 1.618$, the unique positive solution of $x = 1 + 1/x$ forced at T6. The module imports only Constants (for $\varphi$) and Cost, and is marked structural with zero sorry and zero axioms.
In RS units the mass and recognition ladders are powers of $\varphi$. Thresholds built from $\varphi$ and small rationals therefore sit at natural cutoffs between rungs. The sibling domainCost packages a non-negative cost on that ladder; this constant is the numerical bar those costs are compared against.
proof idea
Pure definition: the real constant is written as $\varphi - 3/2$. No lemmas, tactics, or reduction steps.
why it matters
Supplies the fixed cutoff used by the structural certificate RSGRVStructural008Cert and by positivity facts such as canonicalThreshold_pos in the same module. In the broader framework it is a gravity-side companion to other phi-native thresholds (Berry creation at $\varphi^{-1}$, $Z_{\mathrm{cf}} = \varphi^5$). It anchors rung-spacing comparisons without introducing free parameters, consistent with T6 forcing of $\varphi$ and the eight-tick octave geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.