pi_sq_lt
The theorem establishes π² < 9.9225 in the reals by squaring Mathlib's bound π < 3.15. Numerics code in the Recognition framework cites it to obtain a certified upper bound on π squared for interval constructions. The tactic proof obtains the base inequality, applies sq_lt_sq' after confirming positivity, and normalizes the constant 3.15² via norm_num.
claim$π² < 9.9225$
background
The module supplies rigorous bounds on π and its powers by importing Mathlib's proven inequalities such as Real.pi_lt_d2. The upstream Interval structure from Numerics.Interval.Basic is a closed interval with rational endpoints lo ≤ hi. A parallel Interval from Recognition.Certification uses real endpoints lo ≤ hi. These structures support building named intervals such as piSqInterval that contain powers of π.
proof idea
The tactic proof first obtains h := Real.pi_lt_d2 giving π < 3.15 and confirms 0 < π. It then derives π² < 3.15² via sq_lt_sq' and finishes with a calc that rewrites the right-hand side to 9.9225 by norm_num.
why it matters in Recognition Science
This bound feeds the downstream theorem pi_sq_in_interval, which places π² inside piSqInterval. It supplies one of the concrete numeric anchors required by the numerics layer for certified interval arithmetic in Recognition Science, complementing the phi-ladder and J-cost machinery.
scope and limits
- Does not establish any lower bound on π².
- Does not invoke tighter Mathlib bounds such as π < 3.1416.
- Does not prove the inequality inside a custom Interval type.
- Does not address floating-point rounding errors.
Lean usage
example : pi ^ 2 < 9.9225 := pi_sq_ltformal statement (Lean)
115theorem pi_sq_lt : pi ^ 2 < (9.9225 : ℝ) := by
proof body
Tactic-mode proof.
116 have h := Real.pi_lt_d2 -- π < 3.15
117 have hpos : 0 < pi := Real.pi_pos
118 have h1 : pi ^ 2 < (3.15 : ℝ) ^ 2 := sq_lt_sq' (by linarith) h
119 calc pi ^ 2 < (3.15 : ℝ) ^ 2 := h1
120 _ = (9.9225 : ℝ) := by norm_num
121
122/-- Interval containing π² -/