phi_pow_38_interval
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.
claimDefine 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 in Recognition Science
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.
scope and limits
- Does not prove that the exact real value φ^38 lies inside the computed bounds.
- Does not supply a closed-form algebraic expression for φ^38.
- Does not apply when either factor interval has non-positive lower bound.
- Does not tighten the rational approximation of φ beyond the supplied three-decimal interval.
formal statement (Lean)
50def phi_pow_38_interval : Interval :=
proof body
Definition body.
51 mulPos phi_pow_37_interval phiInterval phi_pow_37_lo_pos phi_lo_pos
52