phi_pow_145_interval
plain-language theorem explainer
The definition assembles a closed rational interval for φ^145 by multiplying the intervals for φ^140 and φ^5. Researchers bounding the galactic ratio τ★/τ₀ in Recognition Science numerics cite it to establish that the ratio lies below this power. The construction applies the positive-interval multiplication rule directly to the component intervals and their positivity proofs.
Claim. Let $I_{140}$ be the closed rational interval for φ^140 and $I_5$ the closed rational interval for φ^5, both with positive lower bounds. The interval for φ^145 is then defined by componentwise multiplication: lower endpoint $I_{140}.lo · I_5.lo$ and upper endpoint $I_{140}.hi · I_5.hi$.
background
An Interval is a structure consisting of rational lower and upper bounds with the lower bound at most the upper bound. The mulPos operation computes the product of two such intervals when both have positive lower bounds, setting the new lower bound to the product of the lowers and the upper to the product of the uppers. This definition builds on the interval for φ^140, itself obtained by multiplying intervals for φ^102 and φ^38, and the interval for φ^5 which is explicitly [1109/100, 111/10]. The module context concerns bounding the galactic ratio τ★/τ₀ which is approximately 5.75 × 10^29.
proof idea
The definition is a one-line wrapper applying the mulPos constructor to the φ^140 interval and the φ^5 interval, passing the corresponding positivity lemmas for their lower bounds.
why it matters
This interval definition supports the theorem establishing that the real value φ^145 lies inside it, and the subsequent bound showing the galactic ratio is strictly less than φ^145. It contributes to the phi-ladder computations used for large-scale ratios in the Recognition framework, consistent with the self-similar fixed point φ. No open questions are directly addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.