phi_pow_5_lo_pos
plain-language theorem explainer
The lemma establishes that the lower endpoint of the rational interval for φ^5 is strictly positive. Researchers computing galactic time-scale ratios via interval arithmetic on powers of the golden ratio would cite this to preserve positivity under multiplication. The proof is a one-line term that unfolds the interval definition and reduces the inequality with norm_num.
Claim. $0 < 1109/100$, where the interval for $φ^5$ has lower bound $1109/100$ and upper bound $111/10$.
background
The Numerics.Interval.GalacticBounds module constructs rational intervals to bound high powers of the golden ratio φ for ratios such as τ★ / τ₀ ≈ 5.75e29. The upstream definition phi_pow_5_interval supplies the concrete interval with lo := 1109/100 and hi := 111/10, documented as 'φ^5 interval ≈ 11.09 - PROVEN'. Positivity of the lower bound is required when these intervals are combined via mulPos to form larger exponents.
proof idea
The proof is a one-line term that unfolds phi_pow_5_interval and applies norm_num to verify the rational inequality 1109/100 > 0.
why it matters
This lemma supplies the positivity hypothesis needed by mulPos when constructing phi_pow_37_interval, phi_pow_145_interval and related objects, which in turn feed the containment theorems phi_pow_140_in_interval and phi_pow_145_in_interval. It closes a basic positivity step in the phi-ladder arithmetic used for galactic bounds inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.