phi_lo_pos
plain-language theorem explainer
This lemma establishes that the lower endpoint of the rational interval enclosing the golden ratio is strictly positive. Interval-arithmetic work on phi-ladder scaling for galactic time ratios would cite it when building product intervals. The proof is a one-line term that unfolds the interval definition and applies numerical normalization.
Claim. Let $I$ be the closed rational interval with endpoints $1618/1000$ and $1619/1000$ that contains the golden ratio. Then $0 < I$ lower endpoint.
background
The module supplies numerical interval bounds for the galactic ratio τ★ / τ₀ ≈ 5.75e29. An Interval is a structure with rational endpoints lo and hi satisfying lo ≤ hi. The phiInterval is the concrete instance with lo = 1618/1000 and hi = 1619/1000 that encloses φ = (1 + √5)/2. Upstream results supply the Interval structure and the explicit phiInterval definition.
proof idea
The proof is a one-line term wrapper that unfolds phiInterval to expose the rational lower bound and then applies norm_num to discharge the inequality.
why it matters
The lemma supplies the positivity fact required by mulPos when forming phi_pow_38_interval and phi_pow_38_lo_pos, which in turn feed phi_pow_140_in_interval. It therefore supports the phi-ladder numerics that realize the self-similar fixed point at galactic scales.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.