phi_pow_37_interval
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.