pi_sq_gt
plain-language theorem explainer
9.8596 < π² holds in the reals. Interval-arithmetic code in the Numerics layer cites this to anchor the lower edge of the enclosure for π². The argument reduces the claim to Mathlib's 3.14 < π by applying the monotonicity of squaring on positive reals together with a norm_num identification of the constant.
Claim. $9.8596 < pi^2$ (with the left-hand constant equal to $3.14^2$).
background
This module constructs machine-checked interval enclosures for π and selected powers by importing Mathlib's library of decimal bounds. Real.pi_gt_d2 supplies the fact 3.14 < π while Real.pi_pos guarantees positivity so that the map x ↦ x² remains strictly increasing. The local setting is therefore purely numeric verification: the module builds closed intervals such as piSqInterval that are guaranteed to contain the exact value of π².
proof idea
The proof first obtains 3.14 < π from Real.pi_gt_d2 and 0 < π from Real.pi_pos. It then invokes sq_lt_sq' to conclude 3.14² < π². A norm_num step identifies 9.8596 with 3.14², after which the calc tactic chains the two inequalities.
why it matters
The theorem is invoked inside pi_sq_in_interval to establish that π² lies in piSqInterval. It therefore supplies the lower half of the verified enclosure for π², which the module exports for any downstream numeric argument that requires a rigorous bound on this quantity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.