phi_pow_145_interval
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not verify that the real φ^145 lies within the interval.
- Does not handle intervals with non-positive lower bounds.
- Does not provide a numerical approximation beyond the rational endpoints.
- Does not connect directly to physical constants such as G or alpha.
formal statement (Lean)
70def phi_pow_145_interval : Interval :=
proof body
Definition body.
71 mulPos phi_pow_140_interval phi_pow_5_interval phi_pow_140_lo_pos phi_pow_5_lo_pos
72