piSqInterval
plain-language theorem explainer
This definition supplies the closed rational interval with endpoints 98596/10000 and 99225/10000 that is intended to contain π². Workers on certified numerical methods in the Recognition Science codebase cite it to obtain machine-verified bounds on π squared. The body is a direct structure constructor whose only non-trivial field is discharged by norm_num.
Claim. Let $I$ be the closed interval in the rationals with lower endpoint $98596/10000$ and upper endpoint $99225/10000$, where the ordering of the endpoints is witnessed by normalization.
background
The PiBounds module builds interval enclosures for π and π² by leveraging Mathlib's library of proven inequalities on Real.pi. The Interval type from Numerics.Interval.Basic is a structure carrying rational lower and upper bounds together with a decidable proof of their order. Upstream results include the basic Interval definition and various is predicates from Foundation and GameTheory modules that ensure collision-free or tautological properties in related constructions.
proof idea
The definition is a direct record construction that populates the lo and hi fields with explicit rationals and uses the norm_num tactic to prove the valid field.
why it matters
It is the immediate supplier for the theorem pi_sq_in_interval that certifies containment of π². In the Recognition Science framework this provides a rigorous numerical handle on π that can be combined with the algebraic J-uniqueness and the eight-tick octave without introducing floating-point error. It addresses the need for certified constants in the numerics layer of the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.