four_pi_lt
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 in Recognition Science
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.
scope and limits
- Does not establish any lower bound on 4π.
- Does not derive π from Recognition axioms or the forcing chain.
- Does not extend the bound to complex numbers or other number fields.
Lean usage
have h := four_pi_ltformal statement (Lean)
83theorem four_pi_lt : 4 * pi < (12.6 : ℝ) := by
proof body
Term-mode proof.
84 have h := Real.pi_lt_d2 -- π < 3.15
85 linarith
86
87/-- Interval containing 4π -/