pi_in_piInterval
The declaration shows that π belongs to the closed interval with endpoints 3141592/1000000 and 3141593/1000000. Numerics users in the Recognition framework cite it to anchor interval bounds for trigonometric and algebraic evaluations. The tactic proof reduces the containment predicate via simp, splits the conjunction, and invokes Mathlib's Real.pi_gt_d6 and Real.pi_lt_d6 after norm_num conversion of the rational endpoints.
claimLet $I$ be the interval with lower endpoint $3141592/1000000$ and upper endpoint $3141593/1000000$. Then $3.141592 < pi < 3.141593$ implies $pi$ lies in $I$.
background
The module supplies rigorous interval bounds for π drawing on Mathlib's proven decimal inequalities. The predicate contains, defined as lo ≤ x ≤ hi for an Interval record, checks membership. piInterval is the specific interval with lower bound 3141592/1000000 and upper bound 3141593/1000000, validated by norm_num. Upstream results include Real.pi_gt_d6 (3.141592 < π) and Real.pi_lt_d6 (π < 3.141593) together with the contains definition from Numerics.Interval.Basic.
proof idea
The tactic proof first simplifies the contains predicate over piInterval. It then splits the conjunction into lower and upper bounds. For the lower bound it invokes Real.pi_gt_d6, converts the rational 3141592/1000000 to a real via norm_num, and applies le_of_lt. The upper bound proceeds symmetrically with Real.pi_lt_d6 and the matching conversion.
why it matters in Recognition Science
This result anchors the numerics layer for subsequent interval proofs such as arctan_two_in_interval in the Trig module. It supplies the concrete bounds required by the Recognition framework's interval arithmetic for constants that appear in spacetime emergence. The declaration closes the six-decimal case using external Mathlib facts and feeds directly into trigonometric interval containment.
scope and limits
- Does not establish bounds tighter than six decimal places.
- Does not derive π from Recognition axioms alone.
- Does not extend to complex numbers or higher-precision intervals.
formal statement (Lean)
38theorem pi_in_piInterval : piInterval.contains pi := by
proof body
Tactic-mode proof.
39 simp only [contains, piInterval]
40 constructor
41 · -- 3.141592 ≤ π
42 have h := Real.pi_gt_d6
43 have h1 : ((3141592 / 1000000 : ℚ) : ℝ) < pi := by
44 calc ((3141592 / 1000000 : ℚ) : ℝ) = (3.141592 : ℝ) := by norm_num
45 _ < pi := h
46 exact le_of_lt h1
47 · -- π ≤ 3.141593
48 have h := Real.pi_lt_d6
49 have h1 : pi < ((3141593 / 1000000 : ℚ) : ℝ) := by
50 calc pi < (3.141593 : ℝ) := h
51 _ = ((3141593 / 1000000 : ℚ) : ℝ) := by norm_num
52 exact le_of_lt h1
53
54/-- Wider interval for π: [3.14, 3.15] -/