phi_inv_lt_one
plain-language theorem explainer
The reciprocal of the golden ratio is strictly less than one. Horizon and freeze-out arguments in RS cosmology cite this to unlock geometric-series summability of per-epoch reach. The proof rewrites the quotient inequality using positivity of φ and applies the standing bound 1 < φ.
Claim. With $\varphi$ the golden ratio, $\frac{1}{\varphi} < 1$.
background
This module builds the finite recognition event horizon that drives Phase-9 accelerated-expansion freeze-out. 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,\varphi^{-m}=8(1/\varphi)^m$.
The cumulative reach is the geometric series $\sum_m 8(1/\varphi)^m$. Convergence needs the common ratio strictly below one. Here $\varphi$ is the forced golden ratio from Constants (and the local re-export), already known to satisfy $1<\varphi$ and $\varphi>0$. The reciprocal bound is the missing comparison for Mathlib's geometric-summability lemmas.
proof idea
Term-mode, two steps. Rewrite $1/\varphi<1$ via div_lt_one using positivity of $\varphi$, which reduces the goal to $1<\varphi$. Discharge that by the local one_lt_phi, itself a thin wrapper around Constants.one_lt_phi (proved from $\varphi=(1+\sqrt{5})/2$).
why it matters
Without $1/\varphi<1$ the infinite-epoch reach need not converge, and the de Sitter recognition horizon $8\varphi^2$ would not be forced. Downstream, perEpochReach_summable multiplies Mathlib's geometric summability by the cadence 8, and tsum_phi_inv_pow evaluates $\sum(1/\varphi)^m=\varphi^2$ via the self-similar identity $\varphi^2=\varphi+1$. Together they pin the closed horizon $\sum 8(1/\varphi)^m=8\varphi^2\approx 20.944$ comoving cells, with no fitted Hubble rate. That finite limit is the RS $\Omega_\Lambda$ freeze-out: structure beyond the horizon never enters causal contact. Landmarks: T-6 ($\varphi$ fixed point) and T-7 (eight-tick octave).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.