perEpochReach_summable
plain-language theorem explainer
The per-epoch comoving reach of a recognition signal is a geometric sequence with ratio 1/φ. This lemma records that the sequence is summable over the naturals, the analytic prerequisite for a finite de Sitter recognition horizon 8φ². Anyone citing the Phase-9 freeze-out bound or the real-space reach dichotomy needs it. The proof is a one-line application of the standard geometric-series summability criterion, scaled by the eight-tick cadence.
Claim. The sequence $m \mapsto 8\,(1/\varphi)^m$ is summable over $\mathbb{N}$, where $\varphi$ denotes the golden ratio (self-similar fixed point of the forcing chain).
background
In the recognition-event-horizon module, a recognition signal advances one comoving cell per tick. The eight-tick octave (T7) packs eight cells into each recognition epoch at unit scale. Forced self-similar dilation (T6) stretches the comoving scale by $\varphi$ each epoch, so the distance covered in epoch $m$ is the per-epoch reach $8,(1/\varphi)^m$.
Because $1/\varphi < 1$ (and is nonnegative), the infinite sum of these terms is a classical geometric series. Its sum is the de Sitter recognition event horizon $8\varphi^2 = 8(\varphi+1)\approx 20.944$ comoving cells: no fitted Hubble rate or coupling enters.
Upstream facts used here are exactly the two comparison lemmas $0\le 1/\varphi$ and $1/\varphi < 1$, together with the definition of the per-epoch reach sequence itself.
proof idea
One-line term proof. Apply Mathlib's summable_geometric_of_lt_one to the ratio $1/\varphi$, feeding the local lemmas that $1/\varphi\ge 0$ and $1/\varphi<1$. Then scale the resulting summable geometric sequence on the left by the constant factor 8 (the eight-tick cadence). The result is summability of $m\mapsto 8,(1/\varphi)^m$.
why it matters
Summability is the gate that lets the cumulative reach after infinitely many epochs equal the closed geometric sum $8\varphi^2$. Downstream, cumulativeReach_lt_horizon splits the summable series into a finite partial sum plus a strictly positive tail, proving every finite-epoch reach lies strictly below the horizon. The same fact feeds reach_dichotomy: separations $r<8\varphi^2$ are eventually crossed (and homogenized), while $r\ge 8\varphi^2$ are never crossed (primordial freeze-out).
Framework landmarks: T7 supplies the factor 8; T6 supplies the dilation ratio $1/\varphi$ and the identity $\varphi^2=\varphi+1$ that closes the sum. Together they force the Phase-9 $\Omega_\Lambda$ freeze-out with no free cosmological constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.