pi_pow5_lt_d6
plain-language theorem explainer
The inequality π^5 < 306.0199 follows directly from the library fact π < 3.141593 by monotonicity of the fifth-power map on positive reals and a numerical check. Numerics workers in Recognition Science cite the result when closing interval enclosures for π^5 that appear in expressions for G = φ^5 / π. The proof lifts the base bound via le_of_lt and nlinarith, then chains to the target constant with norm_num.
Claim. $π^5 < 306.0199$
background
The module supplies certified interval bounds for π and its powers by importing Mathlib facts such as Real.pi_lt_d6 (π < 3.141593) and Real.pi_pos. These bounds are assembled for numerical verification inside the Recognition framework, where they feed constants derived from the spacetime interval def interval(v) := ∑_{i:Fin 4} η(i,i) v(i)^2 for a displacement vector v. Upstream, the for structure records a MetaRealizationCert that encodes the structural properties required by self-reference axioms in the unified forcing chain.
proof idea
The tactic proof calls Real.pi_lt_d6 to obtain π < 3.141593 together with Real.pi_pos. It forms the non-strict comparison π ≤ 3.141593 via le_of_lt, then invokes nlinarith on nonnegativity of squares and products to conclude π^5 < (3.141593)^5. A calc chain reduces the goal to a norm_num verification that (3.141593)^5 < 306.0199.
why it matters
The theorem supplies the upper bound required by the downstream result pi_pow5_in_interval_tight, which places π^5 inside piPow5IntervalTight. It supports the numerics layer of the T0-T8 forcing chain, where precise control of π^5 enters G = φ^5 / π and the α^{-1} band (137.030, 137.039). No open scaffolding questions are closed by this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.