phi_pow_140_interval
plain-language theorem explainer
The definition constructs a rational closed interval for φ^140 by multiplying the precomputed intervals for φ^102 and φ^38. Numerics researchers bounding the galactic ratio τ★/τ₀ ≈ 5.75e29 cite it when chaining higher powers of the golden ratio. The construction applies the positive-interval multiplication operator directly to the two factor intervals.
Claim. Let $I_{102}$ be the closed rational interval for φ^{102} and $I_{38}$ the closed rational interval for φ^{38}. The interval for φ^{140} is the product interval whose lower endpoint is the product of the two lower endpoints and whose upper endpoint is the product of the two upper endpoints.
background
The GalacticBounds module computes rational bounds on powers of the golden ratio φ to compare against the galactic ratio τ★/τ₀ ≈ 5.75e29. An Interval is a structure consisting of rational endpoints lo and hi with lo ≤ hi. The mulPos operation multiplies two such intervals when both have positive lower bounds, producing a new interval whose lo is the product of the input los and whose hi is the product of the input his. This declaration depends on the interval for φ^{102} (defined as the square of the φ^{51} interval) and the interval for φ^{38} (defined as the product of the φ^{37} and φ intervals).
proof idea
This is a one-line wrapper that invokes mulPos on the intervals for φ^{102} and φ^{38}, supplying the positivity lemmas for their lower bounds to guarantee the result is a valid positive interval.
why it matters
It feeds the theorems establishing containment of the real φ^{140} and the strict inequality φ^{140} < galactic_ratio, plus the constructions of the intervals for φ^{142} and φ^{145}. This supports numerical verification of the ratio τ★/τ₀ in the Recognition framework, consistent with the self-similar fixed point φ from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.