pi_pow5_in_interval_tight
plain-language theorem explainer
The result places π^5 inside the closed interval with endpoints 306.0193 and 306.0199. Numerics workers building interval enclosures for powers of π cite it to confirm enclosure at d6 precision. The proof reduces the claim to the two strict inequalities on π^5 by simplification and a pair of le_of_lt conversions.
Claim. Let $I$ be the closed interval $[306.0193, 306.0199]$. Then $306.0193 ≤ π^5 ≤ 306.0199$.
background
The module supplies interval enclosures for π and its powers by importing Mathlib's d6 bounds 3.141592 < π < 3.141593. The contains predicate on an interval I and real x asserts that the lower endpoint of I is at most x and x is at most the upper endpoint. The tight interval for π^5 is the one whose endpoints are the rationals 3060193/10000 and 3060199/10000. Upstream theorems establish the strict inequalities 306.0193 < π^5 and π^5 < 306.0199 directly from the d6 bounds on π together with positivity and monotonicity of the fifth-power map.
proof idea
The tactic proof first rewrites the containment goal using the definitions of contains and the target interval. Constructor splits the conjunction into lower and upper subgoals. The lower subgoal applies the theorem giving π^5 > 306.0193, converts the rational endpoint to real, and uses le_of_lt. The upper subgoal applies the companion theorem giving π^5 < 306.0199 and performs the symmetric conversion.
why it matters
The declaration supplies a machine-checked enclosure for π^5 at the d6 level of precision on π. It belongs to the numerics layer that supports interval arithmetic for constants involving 1/π. In the Recognition Science setting it contributes to the handling of G = phi^5 / π and the alpha band by furnishing verified numerical bounds on powers of π. No downstream theorem yet consumes it, so its integration into mass-ladder or forcing-chain calculations remains open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.