pi_sq_lt
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.