phi_pow_32_interval
The definition supplies a rational interval for φ^32 constructed by squaring the precomputed φ^16 interval. Numerics researchers bounding galactic ratios in Recognition Science cite it when chaining to φ^37 and φ^140. The construction applies positive interval multiplication directly to the φ^16 bounds.
claimLet $I_{16}$ denote the closed rational interval containing the real value of the golden ratio raised to the 16th power. The interval for the golden ratio raised to the 32nd power is obtained by multiplying $I_{16}$ with itself under the positive multiplication rule, which sets the new lower bound to the product of the input lower bounds and the new upper bound to the product of the input upper bounds.
background
The module Numerics.Interval.GalacticBounds works with the ratio τ★ / τ₀ ≈ 5.75e29 and relies on closed rational intervals whose endpoints satisfy lo ≤ hi. Positive multiplication of two such intervals is defined by taking the product of their lower endpoints for the result lower bound and the product of their upper endpoints for the result upper bound, provided both input lower bounds are positive. The declaration depends on the φ^16 interval whose rational bounds are 2206.9 and 2207.5 together with the lemma establishing that its lower endpoint is positive.
proof idea
This is a one-line wrapper that applies the positive multiplication operator to the φ^16 interval with itself, passing the positivity lemma for the φ^16 lower bound in both argument positions.
why it matters in Recognition Science
The interval feeds the constructions of φ^37, φ^102, φ^140 and the comparison theorems that place φ^140 below the galactic ratio and establish related inequalities such as 7/10 times the galactic ratio lying below φ^142. It therefore participates in the interval-arithmetic verification of the large-scale ratio that appears in the Recognition Science treatment of galactic time scales. The parent results that consume it are the theorems phi_pow_140_lt_ratio and ratio_0_7_lt_phi_pow_142.
scope and limits
- Does not prove that the real number φ^32 lies inside the produced interval.
- Does not supply bounds for non-integer exponents of the golden ratio.
- Does not connect the interval to any physical mass or length formula beyond the golden-ratio powers themselves.
formal statement (Lean)
34def phi_pow_32_interval : Interval :=
proof body
Definition body.
35 mulPos phi_pow_16_interval phi_pow_16_interval phi_pow_16_lo_pos phi_pow_16_lo_pos
36