piIntervalWide
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.