uses
plain-language theorem explainer
Local alias for the golden ratio in the recognition-event-horizon module. Horizon and per-epoch reach lemmas cite it whenever the self-similar dilation or the closed form $8\varphi^2$ appears. The body is a one-line noncomputable abbrev of the global RS constant.
Claim. Write $\varphi$ for the golden ratio, as a module-local alias of the global Recognition Science constant $\varphi\in\mathbb{R}$.
background
This module sits in RS cosmology and freezes out a finite comoving recognition horizon that drives Phase-9 accelerated-expansion freeze-out. A recognition signal advances one comoving cell per tick; the eight-tick octave (forcing step T7) therefore covers eight cells per epoch at unit scale. Self-similar dilation (T6) stretches the comoving scale by $\varphi$ each epoch, so the reach contributed in epoch $m$ is $8\varphi^{-m}$.
Because $\varphi^{-1}<1$, the infinite geometric series of those contributions converges. The sum is $8\varphi^2=8(\varphi+1)\approx 20.944$ comoving cells: the de Sitter recognition event horizon. No fitted Hubble rate or coupling enters; only the cadence 8 and the identity $\varphi^2=\varphi+1$.
The symbol $\varphi$ is the unique self-similar fixed point forced upstream in the T0–T8 chain. Sibling facts in the module record $\varphi>1$, $\varphi^{-1}\in(0,1)$, and $\varphi^2=\varphi+1$, which turn the series into the closed form $8\varphi^2$.
proof idea
Pure abbreviation: the local symbol is defined to be Constants.phi. No tactic block, no lemmas, no obligations. Downstream lemmas inherit positivity, the bound $\varphi^{-1}<1$, and $\varphi^2=\varphi+1$ from the constants API and from sibling lemmas in this namespace.
why it matters
Every quantitative object in the module is built from this alias: per-epoch reach $8\varphi^{-m}$, its positivity and summability, the cumulative reach, and the horizon value $8\varphi^2$. Those feed the RS account of $\Omega_\Lambda$ freeze-out: separations at or beyond the horizon are never crossed by a recognition signal, so primordial amplitude on those scales cannot homogenize.
Framework landmarks in play are T6 ($\varphi$ as self-similar fixed point) and T7 (eight-tick octave). The module contrasts with past-directed particle-horizon constructions elsewhere: here the future cone and forward epoch sum set the causal cutoff. Broad used_by edges across action convexity, cost algebra, and $\mathbb{Z}[\varphi]$ reflect that the same global $\varphi$ is the RS yardstick; this declaration is the local handle inside the horizon development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.