pi_pow5_lt
plain-language theorem explainer
The inequality π^5 < 312 holds over the reals. Numerics work in the Recognition Science framework cites it when building certified upper bounds on powers of π for interval arithmetic. The proof invokes Mathlib's π < 3.15, lifts the comparison to fifth powers via nlinarith on squares and differences, then finishes with a norm_num check that 3.15^5 < 312.
Claim. $π^5 < 312$
background
The module supplies rigorous interval bounds on π and its powers by importing Mathlib's proven inequalities such as Real.pi_lt_d2 (π < 3.15). The Interval structure (from Basic and Certification) is a closed interval with endpoints lo ≤ hi, used to certify containment of computed values. Upstream Mathlib results include Real.pi_pos and Real.pi_lt_d2, which supply the positivity and strict upper bound needed to compare powers.
proof idea
The tactic proof first obtains h := Real.pi_lt_d2 and hpos := Real.pi_pos. It then proves π^5 < 3.15^5 by le_of_lt on the base bound followed by nlinarith using nonnegativity of squares and (3.15 - π). A calc block chains this to the final norm_num comparison 3.15^5 < 312.
why it matters
The result is used by pi_pow5_in_interval to certify containment of π^5 inside piPow5Interval. It contributes to the module's goal of producing machine-checked interval bounds on π that can be composed with Recognition Science constants such as the phi-ladder and alpha band. No open scaffolding remains for this specific bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.