four_pi_lt_d6
plain-language theorem explainer
The theorem establishes the strict inequality 4π < 12.566372. Numerics researchers building interval arithmetic for Recognition Science constants would cite this result when tightening upper bounds on multiples of π. The proof is a one-line wrapper that imports the Mathlib lemma Real.pi_lt_d6 and applies linarith to scale the bound.
Claim. $4π < 12.566372$ holds in the real numbers, obtained by scaling the Mathlib bound π < 3.141593.
background
The module supplies rigorous interval bounds for π by importing Mathlib's library of proven inequalities such as Real.pi_lt_d6. These bounds are assembled into intervals for π and its powers to support numerical work in the Recognition framework. The local theoretical setting is the construction of tight numeric intervals without relying on external approximations.
proof idea
The term-mode proof obtains the base bound π < 3.141593 via Real.pi_lt_d6, then invokes linarith to conclude the scaled form for 4π.
why it matters
This result feeds the downstream theorem four_pi_in_interval_tight that places 4π inside fourPiIntervalTight. It supplies one of the concrete numeric anchors required by the PiBounds module for later calculations involving constants such as the fine-structure interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.