phi_inv_pos
plain-language theorem explainer
The reciprocal of the golden ratio is strictly positive. Cosmology lemmas on per-epoch recognition reach cite it to keep geometric terms positive. The proof is a one-line application of positivity of reciprocals to the known positivity of φ.
Claim. If $\varphi$ denotes the golden ratio, then $0 < 1/\varphi$.
background
In this module $\varphi$ is the local alias for the golden ratio Constants.phi, the unique positive root of $x^2 = x + 1$. The module already records $\varphi > 0$, $1 < \varphi$, and $\varphi^2 = \varphi + 1$.
The surrounding development builds the recognition event horizon of Phase-9 freeze-out. A recognition signal covers eight comoving cells per epoch (T-7), while self-similar dilation expands the scale by $\varphi$ each epoch (T-6). The comoving distance covered in epoch $m$ is therefore $8(1/\varphi)^m$. Positivity of the dilation ratio $1/\varphi$ is the first arithmetic fact needed before summability and the finite horizon $8\varphi^2$ can be stated.
proof idea
One-line wrapper: Mathlib's one_div_pos reduces $0 < 1/\varphi$ to $0 < \varphi$, which is the already-imported lemma phi_pos (alias of Constants.phi_pos).
why it matters
Feeds two immediate siblings: phi_inv_nonneg (nonnegativity of $1/\varphi$ by le_of_lt) and perEpochReach_pos (each term $8(1/\varphi)^k$ is positive via mul_pos and pow_pos). Those facts underwrite the geometric series for cumulative reach and the finite de Sitter recognition horizon $\sum_m 8(1/\varphi)^m = 8\varphi^2$.
Framework landmarks: T-6 forces $\varphi$ as the self-similar fixed point; T-7 supplies the eight-tick cadence. Together they give the untuned horizon $8\varphi^2 \approx 20.944$ comoving cells that freezes structure beyond causal contact (the RS $\Omega_\Lambda$ freeze-out). Without $1/\varphi > 0$ the per-epoch reach terms are not known positive and the series argument does not start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.