piIntervalWide
piIntervalWide defines the closed rational interval [3.14, 3.15] for π. Numerics code in the Recognition framework cites it when a loose but immediately verifiable enclosure of π is required. The definition is a direct record construction of the Interval structure whose validity condition is discharged by norm_num.
claimThe closed interval $[314/100, 315/100]$ whose rational endpoints satisfy $314/100 ≤ 315/100$.
background
The Interval structure is a record with fields lo : ℚ, hi : ℚ and valid : lo ≤ hi. This module supplies interval enclosures for π by importing Mathlib's proven inequalities such as Real.pi_gt_d2 and Real.pi_lt_d2. The local setting is the construction of rigorous numerical bounds on π and its powers using only verified Mathlib facts.
proof idea
Direct record construction: lo is set to 314/100, hi to 315/100, and the valid field is proved by the norm_num tactic.
why it matters in Recognition Science
The definition supplies the wide interval used by the downstream theorem pi_in_piIntervalWide to prove containment of π. It belongs to the numerics layer that furnishes easily checkable bounds drawn from Mathlib, supporting later interval arithmetic without touching the core T0-T8 forcing chain or J-cost relations.
scope and limits
- Does not supply the tightest Mathlib bounds on π.
- Does not prove any arithmetic property of π beyond the interval definition.
- Does not reference the phi-ladder, J-cost, or Recognition Composition Law.
Lean usage
theorem pi_in_piIntervalWide : piIntervalWide.contains Real.pi := by simp only [contains, piIntervalWide]; constructor; · exact Real.pi_gt_d2; · exact Real.pi_lt_d2formal statement (Lean)
55def piIntervalWide : Interval where
56 lo := 314 / 100 -- 3.14
proof body
Definition body.
57 hi := 315 / 100 -- 3.15
58 valid := by norm_num
59
60/-- π is contained in piIntervalWide - PROVEN -/