canonicalThreshold
plain-language theorem explainer
The canonical sociological threshold is the real constant φ − 3/2. It is the RS-native cutoff against which rates of social change are compared in the Tocqueville-style revolution criterion. Anyone working the Foundation.Sociology revolution-probability statements will cite it as the fixed numerical bar. The declaration is a one-line definitional constant, not a derived theorem.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ denotes the golden-ratio fixed point of the Recognition self-similarity relation.
background
Foundation.Sociology develops an RS reading of Tocqueville: revolution probability spikes when the rate of improvement crosses a fixed multiple of the improvement still needed. The module states the structural claim with zero sorry and zero axiom: the critical scale is tied to $J(\varphi)^{-1}$, with $J$ the unique cost functional $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law.
The constant $\varphi$ is imported from IndisputableMonolith.Constants (T6: the self-similar fixed point). The Cost import supplies the J-cost infrastructure used by sibling lemmas such as domainCost and its nonnegativity. Numerically $\varphi\approx 1.618$, so $\varphi-3/2\approx 0.118$ sits as a small positive bar on the same scale as other RS dimensionless thresholds (Berry creation at $\varphi^{-1}$, dream fraction $\varphi^{-3}$).
proof idea
No proof body. The declaration is a definitional abbreviation: the real constant is introduced by the single equation canonicalThreshold := phi - 3/2. Downstream positivity or comparison lemmas (e.g. the sibling canonicalThreshold_pos) discharge any arithmetic obligations separately.
why it matters
Gives the Sociology module a single named real against which rate-of-change inequalities are written, so the Tocqueville criterion stays dimensionally aligned with the J-cost scale rather than an ad-hoc number. The module framing ties the spike in revolution probability to crossing a $J(\varphi)^{-1}$ threshold; this constant is the concrete numerical stand-in used in that comparison. It sits in the Foundation layer beside the forcing chain landmarks (T5 J-uniqueness, T6 $\varphi$), keeping social-dynamics statements in the same unit system as the rest of the monolith. No downstream used_by edges are recorded yet; sibling certificates (RevProb4Cert, cert) are the natural consumers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.