four_pi_lt
plain-language theorem explainer
The inequality 4π < 12.6 holds over the reals. Numerics code in the Recognition framework cites it to close upper bounds when constructing intervals for multiples of π. The proof is a one-line wrapper that invokes Mathlib's Real.pi_lt_d2 and discharges the rest with linarith.
Claim. $4π < 12.6$
background
The module supplies rigorous bounds on π by importing Mathlib's proven inequalities, including Real.pi_lt_d2 which asserts π < 3.15. The Interval structure from Basic is a closed interval with rational endpoints lo ≤ hi. The Certification version of Interval uses real endpoints lo ≤ hi. These definitions support construction of concrete intervals such as fourPiInterval for downstream Recognition computations.
proof idea
The proof is a one-line wrapper that applies Real.pi_lt_d2 to obtain π < 3.15 and then uses linarith to conclude 4π < 12.6.
why it matters
This theorem supplies the upper bound required by four_pi_in_interval to certify containment of 4π inside fourPiInterval. It forms part of the numerics layer that supports constants appearing in the phi-ladder and the alpha band within the Recognition framework. No open scaffolding questions are addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.