pi_sq_in_interval
plain-language theorem explainer
π² lies inside the closed interval with endpoints 9.8596 and 9.9225. Researchers constructing machine-checked interval arithmetic for powers of π would cite the result when building enclosures for trigonometric constants. The tactic proof unfolds the contains predicate, splits the conjunction, and converts the companion strict inequalities pi_sq_gt and pi_sq_lt into the required non-strict bounds via le_of_lt and calc normalization.
Claim. $9.8596 ≤ π² ≤ 9.9225$, where the endpoints are the rationals 98596/10000 and 99225/10000.
background
The module supplies rigorous interval bounds on π and its powers by importing Mathlib's proven inequalities such as Real.pi_gt_d2 (3.14 < π) and Real.pi_lt_d2 (π < 3.15). The predicate contains, defined in Numerics.Interval.Basic, states that a real number x belongs to an Interval I precisely when I.lo ≤ x ≤ I.hi. The definition piSqInterval constructs the specific interval with lo := 98596/10000 and hi := 99225/10000, justified by the squares of 3.14 and 3.15.
proof idea
The proof applies simp to unfold contains and piSqInterval, then uses constructor to split the conjunction. For the lower bound it invokes pi_sq_gt and converts the strict inequality via le_of_lt inside a calc block that normalizes the rational. The upper bound proceeds symmetrically from pi_sq_lt, again using le_of_lt and norm_num.
why it matters
This result completes the interval enclosure for π² and supports subsequent bounds on higher powers such as π^5 in the same module. It relies on Mathlib's high-precision π bounds to deliver machine-checkable numerics, feeding deterministic claims about constants in the Recognition Science framework. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.