tsum_phi_inv_pow
plain-language theorem explainer
The geometric series of inverse golden-ratio powers sums exactly to φ². Cosmologists and RS auditors cite it when converting the infinite-epoch dilation sum into the closed horizon factor. The proof is the standard geometric-series formula plus the identity φ² = φ + 1.
Claim. The series $\sum_{m=0}^{\infty} (1/\varphi)^m$ converges and equals $\varphi^2$, where $\varphi$ is the golden ratio (the unique positive root of $x^2 = x + 1$).
background
In the Recognition Event Horizon module, a recognition signal covers eight comoving cells per epoch at unit scale (T-7 eight-tick cadence). Self-similar dilation expands the comoving scale by $\varphi$ each epoch (T-6), so the reach in epoch $m$ is $8(1/\varphi)^m$. The infinite sum of those reaches is therefore $8$ times $\sum_m (1/\varphi)^m$.
The golden ratio satisfies $\varphi^2 = \varphi + 1$ (lemma phi_sq_eq from Constants). Because $\varphi > 1$, the ratio $1/\varphi$ is nonnegative and strictly less than one, so the geometric series converges. This lemma isolates the pure dilation sum; the factor of eight is restored downstream.
proof idea
Apply Mathlib's tsum_geometric_of_lt_one with the local facts that $1/\varphi \ge 0$ and $1/\varphi < 1$. The goal reduces to $(1 - 1/\varphi)^{-1} = \varphi^2$. Expand $(1 - 1/\varphi)\varphi^2 = \varphi^2 - \varphi$ by field simplification, rewrite $\varphi^2$ via phi_sq_eq to $\varphi + 1$, and cancel to $1$. Conclude by the right-inverse characterization of multiplicative inverses.
why it matters
This is the algebraic core of the forced de Sitter recognition horizon. Downstream, tsum_perEpochReach multiplies by the eight-tick cadence and obtains $\sum_m \mathrm{perEpochReach}, m = 8\varphi^2 \approx 20.944$ comoving cells: the finite event horizon that drives Phase-9 freeze-out. Structure beyond that scale never enters causal contact and freezes at primordial amplitude (the RS $\Omega_\Lambda$ mechanism).
The only inputs are T-6 ($\varphi$ as self-similar fixed point, via $\varphi^2 = \varphi + 1$) and the geometric-series calculus; there is no fitted Hubble parameter. The module status is fully proved (zero sorry).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.