recognitionEventHorizon
plain-language theorem explainer
The de Sitter recognition event horizon is the closed-form constant $8\varphi^{2}$, the infinite-epoch sum of per-epoch comoving reaches under $\varphi$-dilation. Cosmology and RS freeze-out arguments cite it as the forced causal cutoff for Phase-9 accelerated expansion. The body is a one-line definition: eight-tick cadence times $\varphi^{2}$, with no free parameters.
Claim. The recognition event horizon is the real constant $8\varphi^{2}$ (equivalently $8(\varphi+1)$), the sum $\sum_{m\ge 0} 8\varphi^{-m}$ of per-epoch comoving reaches under unit-tick signaling, eight-tick epochs, and self-similar $\varphi$-dilation per epoch.
background
This module fixes the finite recognition horizon that drives Phase-9 freeze-out. A recognition signal covers one comoving cell per tick. By the eight-tick octave (T7), each epoch covers eight cells at unit scale. Self-similar dilation (T6) expands the comoving scale by $\varphi$ each epoch, so the reach in epoch $m$ is $8\varphi^{-m}$.
Because $1/\varphi<1$, the infinite sum converges: $\sum_{m\ge 0} 8\varphi^{-m}=8/(1-\varphi^{-1})$. The golden-ratio identity $\varphi^{2}=\varphi+1$ rewrites the closed form as $8\varphi^{2}\approx 20.944$ comoving cells. No Hubble rate or coupling is fitted; only the forced cadence $8$ and the dilation sum $\varphi^{2}$.
Sibling quantities are the per-epoch reach $8\varphi^{-m}$ and the partial cumulative reach after $n$ epochs. The horizon is their $n\to\infty$ limit.
proof idea
Definition, not a proved equality. The body sets the constant to $8\varphi^{2}$ in one line. The matching series identity and the rewrite $8\varphi^{2}=8(\varphi+1)$ are discharged later by recognitionEventHorizon_eq via phi_sq_eq. Summability of the geometric terms is handled by sibling lemmas on per-epoch reach.
why it matters
This constant is the arithmetic anchor of RS cosmology freeze-out. Downstream, cumulativeReach_lt_horizon shows every finite partial sum stays strictly below it, so separations at or beyond $8\varphi^{2}$ are never crossed and freeze at primordial amplitude. reach_dichotomy turns that into the real-space split: $r<8\varphi^{2}$ eventually homogenizes; $r\ge 8\varphi^{2}$ never does (the $\Omega_\Lambda$ freeze surface).
horizon_lt_two_pow_five and recognitionEventHorizon_between_dyadic_rungs pin the horizon between $2^4=16$ and $2^5=32$, so dyadic structure freezes exactly at and above rung $5$ with no fitted scale (dyadicFreezeRung_is_least). Framework landmarks: T6 ($\varphi$ fixed point, $\varphi^{2}=\varphi+1$) and T7 (eight-tick octave) supply the only two factors in $8\varphi^{2}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.