phi_pow_37_interval
This definition supplies a rational interval guaranteed to contain φ^37 by multiplying the precomputed intervals for φ^32 and φ^5. Numerics researchers bounding the galactic ratio τ★/τ₀ cite it when extending the phi-power ladder. The construction is a direct application of the positive-interval multiplication operator.
claimLet $I_{32}$ be the closed rational interval for φ^32 and $I_5$ the closed rational interval for φ^5. The interval $I_{37}$ for φ^37 is obtained by endpoint multiplication $I_{37}.lo = I_{32}.lo · I_5.lo$, $I_{37}.hi = I_{32}.hi · I_5.hi$, with validity inherited from the positivity of both lower bounds.
background
The GalacticBounds module approximates the ratio τ★/τ₀ ≈ 5.75e29 by constructing rational intervals over successive powers of the golden ratio φ. Interval is the structure carrying rational lower and upper bounds together with a proof that the lower bound does not exceed the upper. mulPos multiplies two such intervals when both lower bounds are positive, producing new endpoints by direct multiplication and preserving validity. Upstream, phi_pow_32_interval is formed by squaring the φ^16 interval while phi_pow_5_interval is the explicit rational interval [1109/100, 111/10].
proof idea
The definition is a one-line wrapper that applies mulPos to phi_pow_32_interval and phi_pow_5_interval, passing the positivity lemmas phi_pow_32_lo_pos and phi_pow_5_lo_pos to certify that the resulting lower bound remains positive.
why it matters in Recognition Science
phi_pow_37_interval is invoked by phi_pow_38_interval and by the chain that yields phi_pow_140_in_interval together with the comparison theorems phi_pow_140_lt_ratio and phi_pow_142_lt_ratio_1_3. It therefore contributes to the numerical ladder that bounds the galactic ratio against Recognition Science constants. The construction rests on the phi self-similar fixed point and the eight-tick octave from the forcing chain.
scope and limits
- Does not verify that the real number φ^37 lies inside the produced interval.
- Does not compute decimal approximations or floating-point bounds.
- Does not connect the interval to mass-ladder or energy formulas.
- Does not extend the construction to powers beyond 37.
formal statement (Lean)
42def phi_pow_37_interval : Interval :=
proof body
Definition body.
43 mulPos phi_pow_32_interval phi_pow_5_interval phi_pow_32_lo_pos phi_pow_5_lo_pos
44