phi_pow_8_interval
plain-language theorem explainer
This definition supplies the closed rational interval [46.97, 46.99] containing φ^8. Numerics routines for the phi-ladder cite it to bound powers while preserving exact rational endpoints. The construction is a direct structure instantiation whose only obligation is discharged by norm_num.
Claim. Define the closed interval $I = [4697/100, 4699/100]$ such that $I$ contains the real number φ^8, where φ = (1 + √5)/2 is the golden ratio.
background
The Numerics.Interval.Pow module develops interval arithmetic for the power function via the identity x^y = exp(y · log x) for x > 0, with a direct route for natural-number exponents that avoids log/exp. Interval is the structure from Basic consisting of rational endpoints lo, hi together with the proof obligation lo ≤ hi. This declaration re-exports the same numerical bounds already established in PhiBounds.phi_pow8_interval_proven. Upstream results also include the Certification.Interval structure (real endpoints with lo ≤ hi) and the Matches proposition that equates a bridge to a universal dimension-less object.
proof idea
The definition directly instantiates the Interval structure by setting lo := 4697/100 and hi := 4699/100, then discharges the single validity goal with the norm_num tactic. It functions as a one-line wrapper that imports the proven bound from PhiBounds for use inside the Pow module.
why it matters
The interval is consumed by the downstream theorem phi_pow_8_in_interval, which certifies that the concrete real value ((1 + √5)/2)^8 lies inside the declared bounds. It supplies machine-checked numerics support for Recognition Science constants that appear on the phi-ladder, including the eight-tick octave (T7) and the mass-ratio formulas. The declaration closes a small scaffolding step that lets interval arithmetic certify φ^8 without floating-point error.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.