four_pi_gt
plain-language theorem explainer
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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.