four_pi_in_interval_tight
plain-language theorem explainer
Four π lies inside the rational interval with endpoints 12.566368 and 12.566372. Numerics verification steps in Recognition Science cite the result when confirming bounds on π-derived constants. The proof reduces containment to a pair of strict inequalities and discharges each by invoking the supporting d6 bounds on 4π followed by rational normalization.
Claim. Let $I$ be the closed interval with rational endpoints $12.566368$ and $12.566372$. Then $4π$ belongs to $I$.
background
The module supplies rigorous interval bounds on π and its multiples by importing Mathlib's proven inequalities such as 3.141592 < π < 3.141593. The predicate contains states that a real number x satisfies lo ≤ x ≤ hi for an Interval record whose endpoints are rationals. The definition fourPiIntervalTight assembles the specific interval whose lower endpoint is the rational 12566368/1000000 and whose upper endpoint is 12566372/1000000, with validity proved by norm_num.
proof idea
The tactic first simplifies the goal using the definitions of contains and the tight interval. Constructor splits the resulting conjunction. The lower bound invokes the lemma establishing 12.566368 < 4π, converts via le_of_lt, and normalizes the rational endpoint inside a calc block. The upper bound proceeds symmetrically from the companion lemma 4π < 12.566372 and an equational calc that identifies the target rational with its decimal form.
why it matters
The theorem supplies the tight containment statement for 4π inside the PiBounds module, completing the d6-precision verification chain begun by the supporting inequalities. It rests on Mathlib's Real.pi_gt_d6 and Real.pi_lt_d6 together with the basic containment predicate. No immediate downstream theorems are recorded, yet the result contributes verified numerical anchors required for later constants such as powers of π that enter mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.