piInterval
plain-language theorem explainer
piInterval defines the rational interval [3.141592, 3.141593] that contains π. Numerics code inside Recognition Science cites it to obtain error-free bounds on trigonometric functions and powers of π. The definition is a direct record construction whose sole non-trivial obligation is discharged by norm_num.
Claim. Let $I = [3141592/1000000, 3141593/1000000] = [3.141592, 3.141593] subset mathbb{Q}$. Then $I$ is a closed interval satisfying $3.141592 leq pi leq 3.141593$.
background
The module supplies machine-verified rational bounds on π drawn from Mathlib's Real.pi_gt_d6 and Real.pi_lt_d6. Interval is the structure from Numerics.Interval.Basic consisting of rational endpoints lo and hi together with a proof that lo ≤ hi. The same structure appears in Recognition.Certification.Interval but with real endpoints; the present definition uses rationals for exact arithmetic.
proof idea
The definition constructs the Interval record directly with the two rational literals and discharges the validity obligation by norm_num.
why it matters
piInterval supplies the six-decimal bound used by pi_in_piInterval to certify that π lies inside it and by the trigonometric interval arithmetic in Numerics.Interval.Trig to bound arctan(2). It forms part of the chain that replaces floating-point constants with provably correct intervals inside the Recognition Science numerics layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.