phi_pow_38_lo_pos
plain-language theorem explainer
The lemma establishes that the lower endpoint of the rational interval for φ^38 is strictly positive. Numerics constructing the φ^140 interval in the galactic bounds module cite this positivity result to build higher powers. The proof is a term-mode one-liner that unfolds the interval definition and applies the positive-multiplication rule to the already-proved statements for exponents 37 and 1.
Claim. Let $I_{37}$ be the interval for $φ^{37}$ and $I$ the interval for $φ$, both with positive lower bounds. Let $I_{38}$ be the product interval obtained via the positive multiplication operation on $I_{37}$ and $I$. Then $0 < I_{38}.lo$.
background
The GalacticBounds module builds rational intervals for successive powers of the golden ratio to bound the ratio τ★ / τ₀ ≈ 5.75e29. An Interval is a structure with rational endpoints lo and hi satisfying lo ≤ hi. The operation mulPos returns the product interval when both inputs have positive lower bounds, with new lo equal to the product of the input los.
proof idea
The proof is a term-mode one-liner. It unfolds phi_pow_38_interval (defined as mulPos of phi_pow_37_interval and phiInterval) and phi_lo_pos, then applies mul_pos directly to the hypotheses phi_pow_37_lo_pos and phi_lo_pos.
why it matters
This positivity result is required to define phi_pow_140_interval via mulPos on the φ^102 and φ^38 intervals and to prove phi_pow_140_lo_pos. The theorem phi_pow_140_in_interval then certifies that the constructed interval contains the real value goldenRatio^140. It supports numerical certification of high phi-ladder exponents for galactic time-scale ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.