recognition_event_horizon_one_statement
plain-language theorem explainer
Forced φ-dilation (one φ-rung per eight-tick epoch) yields a finite de Sitter recognition horizon 8φ² = 8(φ+1). The tsum of per-epoch reaches equals that horizon; every finite cumulative reach lies strictly below it; and cumulative reach is strictly monotone. Cosmologists citing the RS Phase-9 freeze-out would quote this packaged law. The proof is a four-conjunct term assembling already-proved component lemmas.
Claim. The series $\sum_{m=0}^{\infty}$ of per-epoch comoving reaches equals the recognition event horizon; that horizon equals $8(\varphi+1)$; for every finite epoch count $n$, the cumulative reach after $n$ epochs is strictly less than the horizon; and the map sending $n$ to cumulative reach is strictly monotone on $\mathbb{N}$.
background
This module formalizes the finite recognition horizon that drives Phase-9 accelerated-expansion freeze-out. A recognition signal covers one comoving cell per tick; the eight-tick octave (T-7) therefore contributes eight cells per epoch at unit scale. Forced self-similar dilation expands the comoving scale by $\varphi$ each epoch (T-6), so the comoving distance covered in epoch $m$ is $8/\varphi^m = 8(1/\varphi)^m$.
The cumulative reach after $n$ epochs is the partial sum of those terms. Because $1/\varphi<1$, the infinite geometric series converges to the de Sitter recognition event horizon $8\varphi^2$. The closed form $8\varphi^2=8(\varphi+1)$ uses only the golden-ratio identity $\varphi^2=\varphi+1$; no fitted Hubble rate or coupling enters.
Upstream lemmas already establish: the tsum equals the horizon definition; the closed form via $\varphi^2=\varphi+1$; every partial sum is strictly below the horizon (positive tail of a summable series); and strict monotonicity (each step adds a strictly positive per-epoch reach).
proof idea
Term-mode four-way conjunction. The proof is the anonymous constructor packing four prior results in order: tsum_perEpochReach (infinite sum of per-epoch reaches equals the horizon), recognitionEventHorizon_eq (horizon equals $8(\varphi+1)$ by unfolding and $\varphi^2=\varphi+1$), cumulativeReach_lt_horizon (partial sums stay strictly below via summable tail), and cumulativeReach_strictMono (strict mono from positive per-epoch increments). No new calculation occurs here.
why it matters
Packages the full recognition-event-horizon law into one citation point for the Phase-9 freeze-out story. Module status is theorem with zero sorry and zero RS-internal axiom. The two geometric ingredients are exactly the forcing-chain landmarks T-6 ($\varphi$ as self-similar fixed point, giving dilation $\varphi$ per epoch and $\varphi^2=\varphi+1$) and T-7 (eight-tick octave, giving the prefactor 8). Together they force a finite horizon $\approx 20.944$ comoving cells with no tuned constant.
Physically this is the law-derived freeze-out: any comoving separation at or beyond $8\varphi^2$ is never crossed by a recognition signal, so super-horizon structure freezes at primordial amplitude and supplies the RS $\Omega_\Lambda$ mechanism. Sub-horizon separations are eventually crossed and can homogenize. Downstream real-space reachability dichotomy (Phase 17 in the same module) builds on the same horizon bound. No external used_by edges yet; the declaration is the module's one-statement export.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.