piSqInterval
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove containment of π² inside the interval.
- Does not derive the numerical endpoints from first principles.
- Does not connect the bounds to the phi-ladder or Recognition Composition Law.
formal statement (Lean)
123def piSqInterval : Interval where
124 lo := 98596 / 10000 -- 9.8596
proof body
Definition body.
125 hi := 99225 / 10000 -- 9.9225
126 valid := by norm_num
127
128/-- π² is contained in piSqInterval - PROVEN -/