phi_pow_2_interval
The definition constructs a rational closed interval guaranteed to contain φ² = φ + 1. Numerics researchers bounding galactic mass ratios cite it to propagate interval arithmetic along the phi-ladder. It is realized as a one-line wrapper that adds the precomputed phiInterval to the singleton point interval at 1.
claimDefine the closed rational interval $I_2$ by $I_2 = J + [1]$, where $J$ is the interval with endpoints $1618/1000$ and $1619/1000$ containing the golden ratio φ, so that φ² ∈ $I_2$.
background
Interval is the structure of closed intervals with rational endpoints lo ≤ hi. The point constructor yields the degenerate interval containing exactly one rational. phiInterval is the fixed interval [1618/1000, 1619/1000] containing φ = (1 + √5)/2, established by norm_num bounds on the square root.
proof idea
The definition is a one-line wrapper that applies Interval.add to phiInterval and the point interval at 1.
why it matters in Recognition Science
This supplies the base case for phi_pow_142_interval, which in turn feeds the theorems phi_pow_142_lt_ratio_1_3 and ratio_0_7_lt_phi_pow_142 that bound the galactic ratio τ★/τ₀ ≈ 5.75e29 against φ^142. It closes the exponent-2 step on the phi-ladder (T6) used throughout the Recognition Composition Law.
scope and limits
- Does not prove the interval is the tightest possible.
- Does not extend the bound to real arithmetic beyond the rational endpoints.
- Does not compute explicit numerical values of φ² inside the interval.
formal statement (Lean)
138def phi_pow_2_interval : Interval :=
proof body
Definition body.
139 phiInterval.add (Interval.point 1)
140