four_pi_gt_d6
plain-language theorem explainer
The declaration establishes the strict inequality 4π > 12.566368. Numerics routines that build tight enclosures for multiples of π cite it to certify containment statements. The proof is a one-line wrapper that invokes Mathlib's Real.pi_gt_d6 and closes with linear arithmetic.
Claim. $12.566368 < 4π$
background
The module supplies rigorous interval bounds for π by importing Mathlib's proven decimal inequalities, including Real.pi_gt_d6 which asserts 3.141592 < π. These bounds are assembled into interval objects such as fourPiInterval and fourPiIntervalTight to support exact numerical claims inside the Recognition framework. The local setting is the construction of machine-verified enclosures for π and its powers that later feed constant derivations such as the fine-structure inverse.
proof idea
The proof applies the lemma Real.pi_gt_d6 to obtain 3.141592 < π, then invokes linarith to scale the inequality by four and compare the result against the decimal 12.566368.
why it matters
This bound is used directly by the downstream theorem four_pi_in_interval_tight, which proves that 4π lies inside fourPiIntervalTight. It contributes to the chain of decimal enclosures required for the Recognition Science numerics layer, particularly the interval (137.030, 137.039) that contains α^{-1}.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.