reach_dichotomy
plain-language theorem explainer
A comoving radius is eventually crossed by a recognition signal launched at the seed if and only if it lies strictly below the forced horizon $8\varphi^2$. Cosmologists working Phase-9 freeze-out cite this as the real-space form of the inner homogenized ball versus outer frozen foam split. The proof is a conjunction: a Tendsto argument from the geometric series for the sub-horizon side, and a direct comparison with the strict partial-sum bound for the super-horizon side.
Claim. For every real $r$: if $r < 8\varphi^2$, then there exists a finite epoch $n$ such that the cumulative comoving reach after $n$ epochs exceeds $r$; and if $8\varphi^2 \le r$, then for every finite epoch $n$ the cumulative reach stays strictly below $r$.
background
In this cosmology module a recognition signal covers eight comoving cells per epoch (T-7 eight-tick cadence) while forced self-similar dilation expands the scale by $\varphi$ each epoch (T-6). The per-epoch reach is therefore $8(1/\varphi)^m$. Because $1/\varphi < 1$, the geometric series converges to the recognition event horizon $8\varphi^2 \approx 20.944$ comoving cells; there is no fitted Hubble rate or coupling.
Cumulative reach after $n$ epochs is the partial sum of that series. Upstream results already give: the series is summable; its total sum equals the horizon; and every finite partial sum lies strictly below the horizon. The module formalizes the finite recognition horizon that drives Phase-9 accelerated-expansion freeze-out.
proof idea
Refine into the two conjuncts.
Sub-horizon: summability of per-epoch reach plus the closed-form total sum yield a HasSum at the horizon. The associated partial sums therefore tend to the horizon along atTop. Any $r$ strictly below the horizon is eventually exceeded by those partial sums (eventually_gt_nhds), so some finite $n$ exists.
Super-horizon: apply the already-proved strict inequality that every finite cumulative reach is below the horizon, then compose with $8\varphi^2 \le r$ to keep the cumulative reach below $r$ for all $n$.
why it matters
This is the real-space form of the Phase-9 horizon and the law-derived statement behind the inner homogenized ball / outer frozen foam split used by the cosmogenesis freeze-out scripts. Structure below $8\varphi^2$ is eventually crossed and homogenizes; structure at or beyond never enters causal contact and freezes at primordial amplitude. That is the RS $\Omega_\Lambda$ freeze-out.
The freeze surface is the comoving sphere of radius $8\varphi^2$, which sits strictly between the dyadic shells $2^4=16$ and $2^5=32$. The only ingredients are the cadence 8 (T-7) and the dilation identity $\varphi^2=\varphi+1$ (T-6). No downstream Lean consumers are recorded yet; the declaration closes the freeze-out dichotomy for the real-space foam analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.