pi_sq_in_interval
π² 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 in Recognition Science
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.
scope and limits
- Does not establish the exact value of π.
- Does not provide bounds for π itself, only for its square.
- Does not extend to other powers or constants beyond the listed siblings.
- Does not invoke Recognition Science forcing chain or J-cost.
formal statement (Lean)
129theorem pi_sq_in_interval : piSqInterval.contains (pi ^ 2) := by
proof body
Tactic-mode proof.
130 simp only [contains, piSqInterval]
131 constructor
132 · have h := pi_sq_gt
133 exact le_of_lt (by calc ((98596 / 10000 : ℚ) : ℝ) = (9.8596 : ℝ) := by norm_num
134 _ < pi ^ 2 := h)
135 · have h := pi_sq_lt
136 exact le_of_lt (by calc pi ^ 2 < (9.9225 : ℝ) := h
137 _ = ((99225 / 10000 : ℚ) : ℝ) := by norm_num)
138
139/-! ## Bounds on π⁵ -/
140
141/-- π⁵ = π² · π² · π -/