phi_pow_102_interval
The definition supplies a closed rational interval for φ^102 obtained by squaring the φ^51 interval. Researchers bounding the galactic ratio τ★ / τ₀ ≈ 5.75e29 cite it inside the Recognition Science numerics layer. It is realized by a direct call to the positive-interval multiplication operator on the φ^51 data.
claimLet $I_{51}$ be the closed rational interval containing φ^51. The interval $I_{102}$ for φ^102 is defined by $I_{102} = I_{51} × I_{51}$ via multiplication of positive intervals.
background
The module develops rational interval bounds on powers of the golden ratio φ to constrain the galactic ratio τ★ / τ₀ ≈ 5.75e29. An Interval is a structure with rational endpoints lo ≤ hi. The mulPos operation multiplies two intervals when both lower bounds are positive, setting the product lower and upper bounds and proving validity by monotonicity of multiplication on positives.
proof idea
The definition is a one-line wrapper that applies mulPos to phi_pow_51_interval with itself, passing the positivity witness phi_pow_51_lo_pos twice.
why it matters in Recognition Science
This interval is used to build phi_pow_140_interval and the comparison theorems phi_pow_140_lt_ratio and phi_pow_142_lt_ratio_1_3 that place φ^140 below the galactic ratio. It therefore supports the Recognition Science claim that the phi-ladder and eight-tick octave produce the observed galactic scale. The parent step is the forcing of φ as self-similar fixed point in the unified forcing chain.
scope and limits
- Does not verify that the exact real value φ^102 lies inside the interval.
- Does not extend the construction to non-integer exponents.
- Does not incorporate observational uncertainty from galactic data.
formal statement (Lean)
18def phi_pow_102_interval : Interval :=
proof body
Definition body.
19 mulPos phi_pow_51_interval phi_pow_51_interval phi_pow_51_lo_pos phi_pow_51_lo_pos
20
21/-- φ^16 lo > 0 -/