piInterval
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not establish bounds tighter than six decimal places.
- Does not depend on any Recognition Science axiom or forcing chain step.
- Does not apply to complex or higher-dimensional analogs of π.
- Does not replace Mathlib's higher-precision bounds such as pi_gt_d20.
Lean usage
example : piInterval.contains Real.pi := pi_in_piIntervalformal statement (Lean)
32def piInterval : Interval where
33 lo := 3141592 / 1000000 -- 3.141592
proof body
Definition body.
34 hi := 3141593 / 1000000 -- 3.141593
35 valid := by norm_num
36
37/-- π is contained in piInterval - PROVEN using Mathlib's bounds -/