pi_pow5_in_interval
plain-language theorem explainer
The theorem shows that π raised to the fifth power lies inside the closed interval with rational endpoints 305 and 312. Numerics researchers building interval enclosures for powers of π would cite this result when verifying bounds derived from Mathlib inequalities. The proof reduces containment to a conjunction, invokes the companion strict bounds on π^5, converts them via le_of_lt, and aligns the rational endpoints with norm_num.
Claim. $305 ≤ π^5 ≤ 312$
background
The module supplies rigorous interval bounds on π and its powers by importing Mathlib's proven inequalities such as 3.14 < π < 3.15. The contains predicate states that a real number x belongs to an interval I precisely when the lower endpoint is at most x and x is at most the upper endpoint. The specific interval for π^5 is defined with rational endpoints 305 and 312. Companion results establish the strict inequalities π^5 > 305 using π > 3.14 and π^5 < 312 using π < 3.15.
proof idea
The proof first simplifies the containment statement using the definitions of contains and the interval. It then splits the conjunction into two goals. For the lower bound it applies the theorem establishing π^5 > 305 and converts the strict inequality to a non-strict one with le_of_lt, confirming the left endpoint equals 305 via norm_num. The upper bound is handled symmetrically by invoking the theorem for π^5 < 312 and aligning the right endpoint.
why it matters
This result completes the basic interval enclosure for the fifth power of π within the numerics module. It supports subsequent constructions of interval arithmetic for powers of π that may enter calculations of constants such as the fine-structure constant in the Recognition framework. No downstream uses are recorded yet, but it forms part of the scaffolding for precise numerical verification of the phi-ladder and related quantities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.