phi_inv_nonneg
plain-language theorem explainer
The reciprocal of the golden ratio is nonnegative on the reals. Cosmology proofs that invoke Mathlib geometric-series summability need the weak inequality 0 ≤ 1/φ alongside the strict bound 1/φ < 1. The argument is a one-line lift of the strict positivity lemma via le_of_lt.
Claim. On the reals, $0 \le 1/\varphi$, where $\varphi$ is the golden ratio.
background
The module formalizes the finite recognition event horizon that drives Phase-9 freeze-out. A recognition signal covers eight comoving cells per epoch (T-7 cadence), while self-similar dilation expands the scale by $\varphi$ each epoch (T-6), so the reach in epoch $m$ is $8(1/\varphi)^m$. The cumulative horizon is the geometric series $\sum_m 8(1/\varphi)^m = 8\varphi^2$.
Locally $\varphi$ is an abbreviation for Constants.phi. Upstream lemmas already record $\varphi > 0$, $1 < \varphi$, and $\varphi^2 = \varphi + 1$. The sibling phi_inv_pos states the strict inequality $0 < 1/\varphi$ by one_div_pos applied to positivity of $\varphi$. Mathlib's geometric summability API asks for the weak form $0 \le r$ together with $r < 1$.
proof idea
One-line wrapper: apply le_of_lt to the upstream lemma phi_inv_pos, which already gives $0 < 1/\varphi$. No further algebraic work.
why it matters
Feeds the two geometric-series results that close the horizon formula. perEpochReach_summable invokes Mathlib summable_geometric_of_lt_one with this nonnegativity and phi_inv_lt_one, then multiplies by the cadence 8. tsum_phi_inv_pow uses the same pair to obtain $\sum_m (1/\varphi)^m = (1-1/\varphi)^{-1}$ and rewrites the closed form to $\varphi^2$ via $\varphi^2 = \varphi + 1$.
Those identities deliver the forced de Sitter recognition horizon $8\varphi^2 \approx 20.944$ comoving cells with no fitted Hubble rate. The construction sits on T-6 ($\varphi$ fixed point) and T-7 (eight-tick octave) from the forcing chain; structure beyond the horizon never enters causal contact and freezes as the RS $\Omega_\Lambda$ component.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.