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