canonicalThreshold
plain-language theorem explainer
The canonical threshold is the real constant φ − 3/2, with φ the golden ratio. Cosmology and φ-ladder arguments cite it as the structural cutoff next to domain-cost comparisons in this module. It is a bare definition equating the name to that arithmetic expression; no inequality is proved here.
Claim. Define the canonical threshold by $T_{\mathrm{can}} := \varphi - \tfrac{3}{2}$, where $\varphi$ is the golden ratio (self-similar fixed point of the Recognition forcing chain).
background
Recognition Science forces the golden ratio $\varphi$ as the unique self-similar scale factor (forcing step T6). Adjacent rungs on the RS ladder are separated by the multiplicative factor $\varphi \approx 1.618$. This module records structural cosmology facts about that rung spacing and is marked free of sorry and free of axioms.
Constants supplies $\varphi$; Cost supplies the J-cost infrastructure used by sibling domain-cost definitions in the same file. Those siblings relate evaluation and nonnegativity of a domain cost; the threshold is the fixed real offset placed beside them for comparison and positivity certificates.
proof idea
Definitional only: the real is set equal to $\varphi - 3/2$ by unfolding the imported constant $\varphi$. No tactics, no lemmas, no proof obligations.
why it matters
Structural Module 8 packages RS rung spacing for cosmology. The offset $\varphi - 3/2$ is the natural comparison scale next to domain-cost nonnegativity and the module certificate (siblings such as the positivity lemma for this threshold and the inhabited structural cert). It sits in the ladder geometry forced by T6 (φ) and the eight-tick octave (T7), without claiming an observational bound. Downstream use is local to this structural certificate layer rather than to mass-formula or α-band results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.