canonicalThreshold
plain-language theorem explainer
Defines the real scalar threshold φ − 3/2 used as the canonical cutoff in the J-cost horizon-problem certificate. Cosmologists working the RS 8-tick inflation story cite it when comparing domain cost to the expansion scale. The body is a one-line constant abbreviation in terms of the forced golden ratio.
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
The module treats the classical horizon problem as a structural consequence of the eight-tick (period $2^3$) forcing chain and the J-cost. In Recognition Science, $J(x)=(x+x^{-1})/2-1$ is the unique cost fixed by the Recognition Composition Law; $\varphi$ is the self-similar fixed point forced at T6. Domain cost is the non-negative real obtained by evaluating that cost on a cosmological scale factor ratio.
Module status is a structural theorem with zero sorry and zero axioms: inflation supplies $N_e=44$ e-folds at temperature $T=J(\varphi),T_{\mathrm{Planck}}$, giving an expansion factor $\varphi^{44}\sim 10^9$ that is argued to be consistent with the required $10^{24}$–$10^{26}$ once the $\varphi$-ladder interpretation is fixed. The threshold $\varphi-3/2$ sits just below $\varphi$ and supplies a fixed numerical bar against which domain cost is compared in the certificate.
proof idea
Pure definitional abbreviation: the real constant is written as $\varphi-3/2$ with no proof obligations. Downstream positivity and certificate lemmas unfold this equality and use arithmetic facts about $\varphi>1$.
why it matters
Gives a single named real that the horizon-problem certificate (HorizonProb3Cert and related positivity lemmas in the same module) can quote without re-deriving $\varphi-3/2$ inline. It ties the cosmology layer to the T6 forcing of $\varphi$ and to the eight-tick octave that sets the inflationary e-fold count. The module frames the whole construction as the RS resolution of the horizon problem via J-cost rather than an ad-hoc inflaton potential. No open scaffold remains on this constant itself; it is closed definitional infrastructure for the structural theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.