fourPiInterval
fourPiInterval defines the closed rational interval [12.56, 12.6]. Numerics code in the Recognition framework cites it to enclose 4π for certified interval checks. The definition assigns the two rational endpoints and discharges the ordering constraint with a single norm_num call.
claimThe closed interval $I = [1256/100, 126/10] = [12.56, 12.6]$ whose rational endpoints satisfy $1256/100 ≤ 126/10$.
background
The module supplies interval enclosures for π and its multiples by importing Mathlib's proven bounds such as Real.pi_gt_d2 and Real.pi_lt_d2. Interval is the record structure with fields lo : ℚ, hi : ℚ and valid : lo ≤ hi, defined in Numerics.Interval.Basic and mirrored in Recognition.Certification. This particular definition supplies a coarse but fully certified enclosure for 4π that later theorems can reference directly.
proof idea
The definition is a direct record literal. The only non-trivial field is valid, which is proved by the norm_num tactic normalizing the rational comparison 1256/100 ≤ 126/10.
why it matters in Recognition Science
The interval is consumed by the theorem four_pi_in_interval, which proves containment of 4π. It supports the module's goal of building provably correct numerical bounds on π for use in Recognition Science certification pipelines. The construction relies on Mathlib's high-precision π inequalities rather than any Recognition-specific constants such as phi.
scope and limits
- Does not prove that 4π lies inside the interval (that is the job of four_pi_in_interval).
- Does not supply the tightest possible enclosure for 4π.
- Does not involve Recognition constants such as phi or the eight-tick octave.
- Does not extend automatically to other multiples or powers of π.
Lean usage
example : fourPiInterval.contains (4 * Real.pi) := four_pi_in_intervalformal statement (Lean)
88def fourPiInterval : Interval where
89 lo := 1256 / 100 -- 12.56
proof body
Definition body.
90 hi := 126 / 10 -- 12.6
91 valid := by norm_num
92
93/-- 4π is contained in fourPiInterval - PROVEN -/