phi_pow8_interval_proven
plain-language theorem explainer
This definition supplies the closed rational interval from 46.97 to 46.99 that contains the eighth power of the golden ratio. Numerics work in Recognition Science relies on it to certify bounds for higher powers without external libraries. The proof reduces to a direct construction whose endpoint ordering is settled by norm_num.
Claim. Let $I = [4697/100, 4699/100]$. This is a closed interval with rational endpoints that contains $φ^8$, where $φ = (1 + √5)/2$.
background
The module establishes rigorous bounds on the golden ratio φ = (1 + √5)/2 by first bounding √5 between 2.236 and 2.237 via algebraic comparison of squares, then lifting to bounds on φ itself. An Interval is a structure consisting of rational endpoints lo and hi together with a proof that lo ≤ hi. This definition populates that structure specifically for the eighth power.
proof idea
The definition is a direct record construction that sets the lower endpoint to 4697/100 and the upper endpoint to 4699/100. The validity field is discharged by a single application of norm_num, which confirms the rational inequality between the endpoints.
why it matters
This interval is referenced by the theorem that certifies φ^8 lies inside the bounds and by the Pow module for power-specific intervals. It anchors numerical claims where φ is the self-similar fixed point. The construction supports machine-checked certification of constants appearing in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.