phi_pow_38_interval
plain-language theorem explainer
This definition constructs a rational interval guaranteed to contain φ^38 by multiplying the precomputed interval for φ^37 by the interval for φ itself. Researchers bounding the galactic ratio τ★/τ₀ ≈ 5.75e29 cite this step when chaining intervals to φ^140 and higher. The construction is a direct one-line application of the positive-interval multiplication operator.
Claim. Define the interval $I_{38}$ by componentwise multiplication $I_{38} = I_{37} × I_φ$, where $I_{37}$ is the interval enclosing φ^37 and $I_φ = [1618/1000, 1619/1000]$ encloses φ = (1 + √5)/2, using the positive-interval product that multiplies respective endpoints.
background
Intervals in this module are closed rational intervals used to enclose powers of the golden ratio φ without floating-point error. The Interval structure consists of rational lo and hi endpoints together with a proof that lo ≤ hi. Multiplication of positive intervals is performed by mulPos, which multiplies the lower bounds and upper bounds separately while preserving validity via the monotonicity of multiplication on positives.
proof idea
This is a one-line wrapper that applies mulPos to phi_pow_37_interval and phiInterval, supplying the positivity lemmas phi_pow_37_lo_pos and phi_lo_pos to guarantee the product interval remains valid and positive.
why it matters
This interval is multiplied by phi_pow_102_interval to produce phi_pow_140_interval, which in turn supports the theorems phi_pow_140_lt_ratio and phi_pow_142_lt_ratio_1_3 that bound φ^140 and φ^142 against the galactic ratio. In the Recognition framework it advances the phi-ladder numerics at high exponents, consistent with the self-similar fixed point φ from T6 and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.