phi_pow_16_lo_pos
plain-language theorem explainer
The lemma establishes that the lower endpoint of the explicit rational interval for φ^16 is strictly positive. Numerics researchers building interval arithmetic for high powers of the golden ratio in Recognition Science cite it to propagate positivity through multiplications for exponents like 32 and 140. The proof is a one-line term reduction that unfolds the interval definition and normalizes the rational inequality.
Claim. Let $I_{16}$ be the interval with lower endpoint $2206.9$ and upper endpoint $2207.5$ containing $φ^{16}$. Then the lower endpoint of $I_{16}$ satisfies $2206.9 > 0$.
background
The module Numerics.Interval.GalacticBounds constructs rational intervals for powers of the golden ratio φ to bound the galactic timescale ratio τ★ / τ₀ ≈ 5.75e29. The upstream definition phi_pow_16_interval supplies the concrete bounds lo := 22069/10 and hi := 22075/10, stated to contain φ^16.
proof idea
The proof unfolds phi_pow_16_interval to expose the explicit rational lower bound 22069/10, then applies norm_num to discharge the inequality 22069/10 > 0.
why it matters
This positivity result is invoked directly by phi_pow_32_interval (via mulPos) and by phi_pow_32_lo_pos, which in turn support the containment proof for phi_pow_140_in_interval. It forms part of the phi-ladder interval chain used for high powers in the Recognition framework numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.