phi_pow_37_lo_pos
The lemma shows that the lower endpoint of the rational interval for φ^37 is strictly positive. Numerics constructing the phi-power ladder for galactic ratio bounds cites it to preserve positivity through successive multiplications. The proof is a one-line term that unfolds the mulPos definition of the interval and applies the product-positivity lemma to the already-established lower bounds of the φ^32 and φ^5 intervals.
claimLet $I_{32}$ and $I_5$ be the closed rational intervals for φ^{32} and φ^5 with $I_{32}.lo > 0$ and $I_5.lo > 0$. Define the product interval $I_{37}$ by the positive-multiplication constructor with lower bound $I_{32}.lo · I_5.lo$. Then $I_{37}.lo > 0$.
background
The GalacticBounds module constructs a ladder of rational intervals for successive powers of the golden ratio φ to bound large ratios such as τ★ / τ₀ ≈ 5.75e29. An Interval is a structure carrying rational endpoints lo and hi with lo ≤ hi. The mulPos constructor produces the product interval when both arguments have positive lower bounds, setting the new lo to the product of the input los and the new hi to the product of the input his.
proof idea
Unfold the definition of phi_pow_37_interval, which applies mulPos to phi_pow_32_interval and phi_pow_5_interval. The term then invokes mul_pos on the two upstream positivity lemmas phi_pow_32_lo_pos and phi_pow_5_lo_pos.
why it matters in Recognition Science
The lemma continues the inductive positivity chain for phi-power intervals. It is used directly by the definitions of phi_pow_38_interval and phi_pow_38_lo_pos and by the containment theorem phi_pow_140_in_interval. In the Recognition framework it supports the phi-ladder numerics that appear in mass formulas and galactic bounds, with φ the self-similar fixed point from the forcing chain.
scope and limits
- Does not verify that the interval contains the true real value of φ^37.
- Does not supply floating-point or decimal approximations.
- Does not extend positivity to arbitrary real exponents.
- Does not address rounding or computational error in the endpoints.
Lean usage
unfold phi_pow_38_interval mulPos; dsimp; exact mul_pos phi_pow_37_lo_pos phi_lo_posformal statement (Lean)
45lemma phi_pow_37_lo_pos : (0 : ℚ) < phi_pow_37_interval.lo := by
proof body
Term-mode proof.
46 unfold phi_pow_37_interval mulPos; dsimp
47 exact mul_pos phi_pow_32_lo_pos phi_pow_5_lo_pos
48
49/-- Interval for φ^38 = φ^37 * φ^1 -/