pi_pow5_in_interval
π^5 lies in the closed interval with endpoints 305 and 312. Workers verifying numerical constants derived from powers of π in Recognition Science would cite the result when bounding expressions such as G = φ^5 / π. The tactic proof reduces the containment predicate to a pair of inequalities and converts the companion strict bounds via le_of_lt.
claim$305 ≤ π^5 ≤ 312$
background
The module builds interval arithmetic facts for π and its powers from Mathlib's proven decimal bounds. The containment predicate states that a real number x belongs to an interval I precisely when the lower endpoint is at most x and x is at most the upper endpoint. The specific interval for π^5 is the closed interval whose rational endpoints are 305 and 312. Upstream lemmas establish the strict inequalities π^5 > 305 (using π > 3.14) and π^5 < 312 (using π < 3.15).
proof idea
The proof normalizes the containment predicate to the conjunction of the two endpoint inequalities. It invokes the lower-bound lemma to obtain a strict inequality, converts it to the required non-strict form with le_of_lt inside a calc block, and repeats the process for the upper bound using the symmetric upper-bound lemma.
why it matters in Recognition Science
The result supplies a verified numerical anchor for the fifth power of π inside the interval layer. It supports downstream constant checks that rely on bounded powers of π, including the expression G = φ^5 / π that appears in the Recognition Science derivation of Newton's constant. No direct parent theorems are recorded, yet the fact closes one link in the chain of interval facts needed for alpha-band and phi-ladder numerical validation.
scope and limits
- Does not supply bounds tighter than the d2 decimal precision on π.
- Does not treat containment for any exponent other than five.
- Does not connect the interval to the J-cost function or the phi-ladder.
- Does not generalize the method to arbitrary real powers.
formal statement (Lean)
176theorem pi_pow5_in_interval : piPow5Interval.contains (pi ^ 5) := by
proof body
Tactic-mode proof.
177 simp only [contains, piPow5Interval]
178 constructor
179 · have h := pi_pow5_gt
180 exact le_of_lt (by calc ((305 : ℚ) : ℝ) = (305 : ℝ) := by norm_num
181 _ < pi ^ 5 := h)
182 · have h := pi_pow5_lt
183 exact le_of_lt (by calc pi ^ 5 < (312 : ℝ) := h
184 _ = ((312 : ℚ) : ℝ) := by norm_num)
185
186/-! ## Tighter bounds using d6 precision -/
187
188/-- 4π > 12.566368 (using π > 3.141592) -/