phi_pow_142_interval
This definition supplies a closed rational interval containing φ^142 by multiplying the precomputed intervals for φ^140 and φ^2. Galactic timescale calculations cite the bound when placing the observed ratio τ★/τ₀ on the φ-ladder at rung 142. The implementation is a direct one-line wrapper that applies the positive-interval multiplication operator together with the two lower-power positivity lemmas.
claimLet $I_{142}$ be the closed interval with rational endpoints given by the product of the intervals for φ^{140} and φ^2, where both factors lie in the positive reals and φ denotes the golden ratio.
background
The module Numerics.Interval.GalacticBounds constructs rational intervals that sandwich successive powers of the golden ratio φ. An Interval is a structure with rational lower and upper bounds together with a proof that the lower bound does not exceed the upper bound. The operator mulPos multiplies two such intervals when both have positive lower bounds, returning the interval whose endpoints are the products of the respective bounds.
proof idea
The definition is a one-line wrapper that invokes mulPos on phi_pow_140_interval and phi_pow_2_interval, supplying the positivity lemmas phi_pow_140_lo_pos and phi_pow_2_lo_pos to guarantee the resulting interval is well-defined.
why it matters in Recognition Science
This interval feeds the theorem tau_star_is_phi_rung asserting that the galactic timescale ratio lies within 10 percent of the φ^142 rung. It also supports the membership proof phi_pow_142_in_interval and the bounding comparisons phi_pow_142_lt_ratio_1_3 and ratio_0_7_lt_phi_pow_142. In the Recognition framework the construction helps verify that the observed galactic ratio is forced by the self-similar fixed point φ at the eight-tick octave scale.
scope and limits
- Does not compute the exact real value of φ^142.
- Does not prove that the interval is the tightest possible rational bound.
- Does not extend to non-positive intervals.
- Does not address powers outside the supplied multiplication chain.
formal statement (Lean)
145def phi_pow_142_interval : Interval :=
proof body
Definition body.
146 mulPos phi_pow_140_interval phi_pow_2_interval phi_pow_140_lo_pos phi_pow_2_lo_pos
147