canonicalThreshold
plain-language theorem explainer
Defines the canonical real threshold as φ − 3/2, a fixed RS-native cutoff used in the Module 11 cosmology bookkeeping for ISM dust. Cosmologists citing the structural dust-fraction match will pull this constant rather than hard-coding the shift. The body is a one-line definitional abbreviation of the golden ratio minus three halves.
Claim. The canonical threshold is the real number $\varphi - 3/2$, where $\varphi$ is the golden-ratio fixed point of the Recognition self-similarity relation.
background
Module 11 of the RS cosmology stack treats the interstellar-medium dust fraction as a structural prediction: $J(\varphi)^2 \approx 1.39%$, compared with the empirical $\sim 1%$ band. The module is marked as a structural theorem (zero sorry, zero axiom).
Here $\varphi$ is the unique self-similar fixed point forced at T6 of the Unified Forcing Chain, and $J$ is the unique cost functional $J(x)=(x+x^{-1})/2-1$ from T5 (equivalently $\cosh(\log x)-1$). The Cost and Constants imports supply those primitives; this declaration only names a real shift of $\varphi$ used as a comparison threshold in the local domain-cost calculus.
proof idea
Definitional. The right-hand side is the literal real expression $\varphi - 3/2$; there is no proof obligation beyond the ambient real arithmetic of Mathlib and the imported constant $\varphi$.
why it matters
Gives a single named real for the Module 11 dust-fraction story so sibling lemmas (nonnegativity and positivity of the threshold, the domain-cost evaluation, and the RSCosmo011 certificate) can cite one symbol instead of an inline shift. It sits inside the cosmology domain that converts the forced $\varphi$-ladder and $J$-cost into an ISM dust percentage claimed to match observation. No forcing-chain step is proved here; the declaration is pure scaffolding for that structural match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.