phi_pow_2_lo_pos
plain-language theorem explainer
The lemma establishes that the lower endpoint of the rational interval approximating φ² exceeds zero. Numerics researchers bounding galactic time ratios via high powers of the golden ratio cite it to guarantee positivity under interval multiplication. The proof is a one-line term that unfolds the interval definition and applies norm_num to the resulting rational comparison.
Claim. $0 < I_{φ^2}.lo$ where $I_{φ^2}$ is the closed rational interval obtained by adding the point interval $[1,1]$ to the interval containing $φ = (1 + √5)/2$.
background
The module constructs rational intervals for powers of the golden ratio to bound the galactic ratio τ★ / τ₀ ≈ 5.75e29. Interval is the structure with fields lo, hi : ℚ and valid : lo ≤ hi. phiInterval is the rational interval [1618/1000, 1619/1000] containing φ. phi_pow_2_interval is defined as phiInterval.add (Interval.point 1), which encodes the identity φ² = φ + 1. The upstream structure for from UniversalForcingSelfReference records meta-realization properties that justify the self-similar use of φ.
proof idea
The term proof unfolds phi_pow_2_interval and phiInterval, then invokes norm_num to verify the concrete rational inequality 0 < 1618/1000.
why it matters
The lemma supplies the positivity witness required by mulPos in the definition of phi_pow_142_interval, which is then used by phi_pow_142_in_interval to certify that the interval contains goldenRatio^142. It therefore closes a numerical step in the chain that produces the galactic bound, linking to the self-similar fixed point φ (T6) and the eight-tick octave structure of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.