phi_pow_2_interval
plain-language theorem explainer
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.
Claim. Define 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.