phi_pow_140_in_interval
plain-language theorem explainer
The theorem shows that the golden ratio to the 140th power lies inside a pre-defined interval constructed for that exponent. Numerics researchers bounding the galactic ratio τ★/τ₀ ≈ 5.75e29 would cite it when chaining phi-ladder containments. The proof builds the result by deriving containments for 51, 102, 16, 32, 5, 37, 38 and finally combining the 102 and 38 intervals via repeated application of the positive-interval multiplication lemma.
Claim. Let φ be the golden ratio. Let I_{140} be the interval obtained as the positive product of the intervals for φ^{102} and φ^{38}. Then φ^{140} satisfies I_{140}.lo ≤ φ^{140} ≤ I_{140}.hi.
background
The module Numerics.Interval.GalacticBounds supplies intervals that bound successive powers of the golden ratio for estimating the galactic ratio τ★/τ₀ ≈ 5.75e29. The predicate contains(I, x) holds precisely when the lower endpoint of I is ≤ x and x is ≤ the upper endpoint. The supporting lemma mulPos_contains_mul states that if two intervals have positive lower bounds and contain x and y, then their product interval contains the product x y. Upstream results include the base containment phi_pow_51_in_interval together with the positivity lemmas phi_lo_pos and phi_pow_16_lo_pos.
proof idea
The tactic proof first obtains the containment for exponent 51, squares it to reach 102, squares the 16-interval to reach 32, multiplies the 32- and 5-intervals to reach 37, multiplies the 37- and 1-intervals to reach 38, and finally multiplies the 102- and 38-intervals to reach 140. Each multiplication step invokes mulPos_contains_mul after rewriting the exponent sum via Real.rpow_add.
why it matters
The result is invoked directly by phi_pow_140_lt_ratio to conclude φ^{140} < galactic_ratio_rational and by the containments for exponents 142 and 145. It supplies a concrete numerical link in the phi-ladder used to bound the galactic ratio inside the Recognition Science framework. The construction closes one step of the interval arithmetic needed to compare φ-powers against the target ratio 5.75e29.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.