pi_pow5_gt_d6
plain-language theorem explainer
This result supplies the strict lower bound 306.0193 < pi^5. Numerics work inside the Recognition Science project cites it when tightening containment intervals for powers of pi. The tactic proof lifts Mathlib's sixth-decimal lower bound on pi to the fifth power by nlinarith on squared non-negative terms followed by a calc chain.
Claim. $306.0193 < pi^5$, obtained by lifting the inequality $3.141592 < pi$ through the monotonicity of the fifth-power map on the positive reals.
background
The module Numerics.Interval.PiBounds constructs interval bounds on pi and its powers by importing Mathlib's library of proven inequalities. Key resources include Real.pi_gt_d6, which asserts 3.141592 < pi, together with similar bounds at other decimal precisions up to twenty places. These support constructions such as piPow5IntervalTight for numerical verification of constants that involve pi.
proof idea
The tactic proof first invokes Real.pi_gt_d6 to obtain 3.141592 < pi. It then proves (3.141592)^5 < pi^5 by applying nlinarith to the non-negative quantities sq_nonneg pi, sq_nonneg (pi - 3.141592) and the corresponding higher-power terms. A final calc block combines a norm_num fact on (3.141592)^5 with the lifted inequality.
why it matters
The theorem is used by pi_pow5_in_interval_tight to establish that pi^5 lies inside piPow5IntervalTight. It supplies a concrete numerical step that supports computations of constants such as G = phi^5 / pi inside the Recognition Science framework. The bound closes a gap in the numerics layer without adding new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.