phi_pow_140_interval
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish that the real φ^{140} lies inside the interval
- Does not compute the numerical value of the interval endpoints
- Relies on positivity of the factor intervals
- Specific to exponent 140
formal statement (Lean)
62def phi_pow_140_interval : Interval :=
proof body
Definition body.
63 mulPos phi_pow_102_interval phi_pow_38_interval phi_pow_102_lo_pos phi_pow_38_lo_pos
64