four_pi_gt
12.56 < 4π holds over the reals. Interval-arithmetic code in numerics cites this to anchor the lower bound when constructing fourPiInterval. The proof obtains 3.14 < π from Mathlib and closes the target inequality by linear arithmetic.
claim$12.56 < 4π$
background
The module supplies rigorous interval bounds on π by importing Mathlib's proven inequalities, including Real.pi_gt_d2 which asserts 3.14 < π. Local conventions treat these bounds as the foundation for intervals on π and its powers, with no additional Recognition Science primitives required. The setting is purely numerical verification to support downstream interval membership proofs.
proof idea
The proof is a short tactic sequence. It obtains the hypothesis 3.14 < π via Real.pi_gt_d2, then applies linarith to deduce 12.56 < 4π.
why it matters in Recognition Science
The result is invoked directly by four_pi_in_interval to establish membership of 4π in fourPiInterval. It supplies a concrete numerical anchor inside the numerics layer that feeds interval arithmetic for constants appearing in mass formulas and related calculations. No open questions or scaffolding are involved.
scope and limits
- Does not establish any upper bound on 4π.
- Does not extend the bound to other multiples or to powers of π.
- Does not invoke Recognition Science axioms or forcing-chain steps.
Lean usage
have h := four_pi_gtformal statement (Lean)
78theorem four_pi_gt : (12.56 : ℝ) < 4 * pi := by
proof body
Term-mode proof.
79 have h := Real.pi_gt_d2 -- 3.14 < π
80 linarith
81
82/-- 4π < 12.6 -/