phi_pow_16_lo_pos
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove that the given interval actually contains the real value of φ^16.
- Does not supply bounds or positivity for any exponent other than 16.
- Does not address interval arithmetic operations beyond the lower-bound check.
Lean usage
lemma phi_pow_32_lo_pos : (0 : ℚ) < phi_pow_32_interval.lo := by unfold phi_pow_32_interval mulPos; dsimp; exact mul_pos phi_pow_16_lo_pos phi_pow_16_lo_posformal statement (Lean)
22lemma phi_pow_16_lo_pos : (0 : ℚ) < phi_pow_16_interval.lo := by
proof body
Term-mode proof.
23 unfold phi_pow_16_interval; norm_num
24
25/-- φ^5 lo > 0 -/