at
plain-language theorem explainer
Packages the real-space Phase-9 freeze surface: inside the comoving sphere of radius $8\varphi^2$ recognition eventually homogenizes structure; at and beyond that radius no finite epoch arrives, so amplitudes freeze. Cosmologists cite it for the inner homogenized ball / outer frozen foam split. It is a structure definition (no proof body), built from the eight-tick cadence and the $\varphi$-dilation geometric series.
Claim. A structure asserting the real-space recognition horizon: for every comoving radius $r < 8\varphi^2$, structure at $r$ is eventually homogenized, while for every $r \ge 8\varphi^2$ no finite epoch reaches $r$, so structure freezes at its primordial amplitude. The freeze surface is the sphere of radius $8\varphi^2$, strictly between the dyadic shells $2^4 = 16$ and $2^5 = 32$.
background
This module fixes the finite recognition event horizon that drives Phase-9 accelerated-expansion freeze-out. A recognition signal advances one comoving cell per tick. By the eight-tick octave (T7), one epoch covers eight cells at unit scale. Self-similar dilation expands the comoving scale by $\varphi$ each epoch (T6), so the reach in epoch $m$ is
$$\mathrm{perEpochReach}(m) = 8,\varphi^{-m}.$$
The infinite-horizon cumulative reach is the geometric series $\sum_{m\ge 0} 8\varphi^{-m}$. Since $\varphi^{-1}<1$, it converges to $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 forced cadence 8 and the identity $\varphi^2=\varphi+1$.
Partial sums stay strictly below $8\varphi^2$ and increase monotonically. Separations at or beyond the horizon are never crossed, so they cannot homogenize. That is the RS $\Omega_\Lambda$ freeze-out, distinct from the past-directed particle horizon treated in VacuumHorizonForcing.
proof idea
Definitional structure, not a proved theorem: no tactic script and no sorry. The mathematical content is the closed form of the geometric series for cumulative reach,
$$\sum_{m\ge 0} 8\varphi^{-m} = 8/(1-\varphi^{-1}) = 8\varphi^2,$$
together with the elementary comparison that every finite partial sum is $< 8\varphi^2$ while the limit equals it. Sibling facts supply $\varphi>1$, $\varphi^{-1}\in(0,1)$, positivity and summability of per-epoch reach, and the identity $\varphi^2=\varphi+1$. The structure records the resulting dichotomy (eventual homogenization for $r<8\varphi^2$ versus permanent freeze for $r\ge 8\varphi^2$) as the real-space form of that horizon.
why it matters
Gives the law-derived freeze surface behind the inner homogenized ball / outer frozen foam split used by the cosmogenesis real-space freeze-out scripts. The two inputs are framework landmarks only: T7 (eight-tick octave) fixing the prefactor 8, and T6 ($\varphi$ as self-similar fixed point, $\varphi^2=\varphi+1$) fixing the dilation sum. The horizon value $8\varphi^2$ sits cleanly between dyadic shells 16 and 32, so the split is stable under integer shell bookkeeping.
Physically this is the RS account of $\Omega_\Lambda$ freeze-out: structure beyond the recognition horizon never enters causal contact and retains primordial amplitude, while interior structure is eventually crossed and homogenized. The module status is theorem-grade (0 sorry, 0 RS-internal axiom) for the supporting reach lemmas; this declaration is the packaging structure for the real-space dichotomy. No downstream Lean consumers are wired yet in the graph; the immediate consumers are the Phase-9 cosmology scripts and any later theorem that quotes the freeze radius explicitly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.