pi_pow5_gt
plain-language theorem explainer
The result proves that pi raised to the fifth power is greater than 305 in the reals. Interval arithmetic specialists in Recognition Science numerics cite it to anchor lower bounds on pi powers. The proof reduces the claim to a numerical comparison after invoking the external bound pi greater than 3.14 and applying monotonicity via a nonlinear arithmetic solver.
Claim. The real number $pi$ satisfies $pi^5 > 305$.
background
The module develops rigorous bounds on pi and its integer powers using Mathlib's library of proven inequalities, including the fact that pi exceeds 3.14. This supplies the local setting for interval containment statements that support numerical verification throughout the Recognition Science framework. The present declaration requires no internal upstream lemmas and depends only on the imported bound pi greater than 3.14.
proof idea
The tactic proof first obtains the inequality that pi exceeds 3.14 from the imported library. It then proves that 3.14 to the fifth is strictly less than pi to the fifth by applying a nonlinear arithmetic solver to nonnegativity facts about squares and differences. A final calculation chain establishes that 305 is less than 3.14 to the fifth, which is less than pi to the fifth.
why it matters
This lower bound is invoked by the companion result that places pi to the fifth inside the target interval. It contributes to the numerics infrastructure that verifies constants such as the inverse fine structure constant within the interval from 137.030 to 137.039. The declaration supports the overall forcing chain by providing concrete numerical anchors for the phi-ladder and related mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.