cumulativeReach_strictMono
plain-language theorem explainer
The cumulative comoving reach after n epochs is strictly increasing in n. Cosmologists citing the RS Phase-9 freeze-out use this to guarantee the causal frontier advances every epoch. The proof reduces StrictMono on ℕ to the successor step, rewrites the partial sum, and closes by positivity of each per-epoch term.
Claim. The map $n \mapsto R_n$ is strictly monotone on $\mathbb{N}$, where $R_n=\sum_{m=0}^{n-1} 8\,\varphi^{-m}$ is the cumulative comoving reach after $n$ recognition epochs (each summand the cadence-eight reach dilated by $\varphi^m$).
background
The Recognition Event Horizon module formalizes a finite de Sitter horizon forced by φ-dilation, with no fitted Hubble rate. A recognition signal covers eight comoving cells per epoch (T-7 eight-tick cadence). Forced self-similar dilation expands the comoving scale by φ each epoch (T-6), so the distance covered in epoch m is $8/\varphi^m=8(1/\varphi)^m$.
Cumulative reach after n epochs is the partial sum of those per-epoch terms. Because $1/\varphi<1$, the series converges to $8\varphi^2=8(\varphi+1)$. The module's physical claim is that partial reaches stay strictly below this horizon and climb toward it, so separations at or beyond the horizon never enter causal contact.
Upstream, each summand is already known to be strictly positive: the factor 8 is positive and $(1/\varphi)^k>0$ by positivity of the inverse golden ratio.
proof idea
Apply Mathlib's criterion that a function on ℕ is strictly monotone once $f(n)<f(n+1)$ for every n. For the successor step, rewrite the $(n+1)$-st partial sum as the n-th sum plus the n-th summand via the range-successor identity for Finset sums. The added term is strictly positive by the per-epoch positivity lemma, so a linear-arithmetic close finishes the inequality.
why it matters
Feeds the packaged theorem recognition_event_horizon_one_statement, which asserts four facts together: the series sums to the horizon, the horizon equals $8(\varphi+1)$, every partial sum lies strictly below the horizon, and the cumulative reach is strictly monotone. That package is the law-derived freeze-out for Phase-9 accelerated expansion: structure beyond $8\varphi^2$ is never crossed by a recognition signal and freezes at primordial amplitude.
Strict monotonicity is the half that says the causal frontier advances every epoch rather than stalling. Combined with the below-horizon bound, sub-horizon modes are eventually homogenized while super-horizon modes remain frozen. The only framework inputs are T-6 (φ as self-similar fixed point, via $\varphi^2=\varphi+1$) and T-7 (eight-tick octave as the cadence 8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.