four_pi_in_interval
The declaration shows that 4π lies inside the closed interval with endpoints 12.56 and 12.6. Code performing interval arithmetic over multiples of π in Recognition Science numerics would cite this result to certify containment. The proof is a short tactic script that unfolds the interval definition, splits the two-sided inequality, and reduces each side to one of the supporting lemmas four_pi_gt or four_pi_lt via rational normalization.
claim$4π$ satisfies $12.56 ≤ 4π ≤ 12.6$, where the interval is the one whose lower endpoint is the rational 1256/100 and whose upper endpoint is the rational 126/10.
background
The module supplies certified interval bounds on π by importing Mathlib's proven inequalities (π > 3.14 and π < 3.15). The contains predicate, defined in Interval.Basic, states that a real number x belongs to an interval I precisely when the lower bound of I is ≤ x and x is ≤ the upper bound of I. fourPiInterval is the concrete interval whose lower bound is 1256/100 and upper bound is 126/10, with validity proved by norm_num.
proof idea
simp unfolds contains and fourPiInterval to expose the two-sided inequality. constructor splits the goal into lower and upper parts. The lower part calls four_pi_gt, rewrites 1256/100 to 12.56, and applies le_of_lt. The upper part calls four_pi_lt, rewrites 4 * pi < 12.6, and normalizes 126/10 to 12.6 before applying le_of_lt.
why it matters in Recognition Science
The theorem closes the containment statement for the four-pi interval inside the Numerics.Interval.PiBounds module. It supplies a proved fact that any later numeric calculation requiring a certified bound on 4π can invoke directly. The result sits downstream of the Mathlib π bounds and the local four_pi_gt / four_pi_lt lemmas; no further parent theorems are recorded in the dependency graph.
scope and limits
- Does not establish bounds tighter than two decimal places.
- Does not apply to other multiples of π or to π itself.
- Does not incorporate higher-precision Mathlib bounds such as pi_gt_d20.
- Does not address interval arithmetic over complex numbers or vectors.
formal statement (Lean)
94theorem four_pi_in_interval : fourPiInterval.contains (4 * pi) := by
proof body
Tactic-mode proof.
95 simp only [contains, fourPiInterval]
96 constructor
97 · have h := four_pi_gt
98 exact le_of_lt (by calc ((1256 / 100 : ℚ) : ℝ) = (12.56 : ℝ) := by norm_num
99 _ < 4 * pi := h)
100 · have h := four_pi_lt
101 exact le_of_lt (by calc 4 * pi < (12.6 : ℝ) := h
102 _ = ((126 / 10 : ℚ) : ℝ) := by norm_num)
103
104/-! ## Bounds on π² -/
105
106/-- π² > 9.8596 (using 3.14² = 9.8596) -/