pi_in_piInterval
plain-language theorem explainer
π satisfies the six-decimal enclosure with lower endpoint 3141592/1000000 and upper endpoint 3141593/1000000. Numerics code inside the Recognition Science stack cites this enclosure when building interval bounds for trigonometric functions. The proof reduces the containment predicate by simplification, splits the resulting conjunction, and invokes Mathlib's Real.pi_gt_d6 together with Real.pi_lt_d6 after rational-to-real conversion via norm_num.
Claim. $3141592/1000000 ≤ π ≤ 3141593/1000000$
background
The contains predicate, defined in the Basic interval module, states that a real number x lies in an interval I precisely when the lower endpoint is at most x and x is at most the upper endpoint. The piInterval definition constructs the concrete interval whose lower bound is the rational 3141592/1000000 and whose upper bound is 3141593/1000000, with validity established by norm_num. This module supplies rigorous bounds on π by importing and applying Mathlib's library of decimal inequalities.
proof idea
The tactic proof first simplifies the goal with respect to the definitions of contains and piInterval. Constructor splits the resulting conjunction into lower-bound and upper-bound subgoals. The lower subgoal converts the rational 3141592/1000000 to a real, applies the Mathlib lemma Real.pi_gt_d6, and closes with le_of_lt. The upper subgoal proceeds symmetrically with Real.pi_lt_d6 and norm_num for the equality step.
why it matters
This result supplies the verified six-decimal enclosure for π that the Trig submodule uses when proving interval membership statements such as arctan(2) belonging to its target interval. It implements the precise bounds catalogued in the module documentation, enabling safe composition of interval expressions for constants that appear in physical calculations. Within the Recognition framework the enclosure supports numerical consistency checks in the numerics layer without reliance on floating-point approximations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.