piPow5Interval
plain-language theorem explainer
piPow5Interval supplies the closed rational interval [305, 312] asserted to contain π^5. Numerics researchers building enclosures for powers of π inside the Recognition Science stack cite this definition when composing interval certificates for constants such as alpha. The construction is a direct record literal whose only obligation is discharged by norm_num.
Claim. Define the closed interval $I = [305, 312]subseteqmathbb{Q}$ whose rational endpoints satisfy $305leq 312$.
background
The module Numerics.Interval.PiBounds assembles rigorous rational enclosures for π and its powers by importing Mathlib's proven bounds such as Real.pi_gt_d20. An Interval is the structure with fields lo : ℚ, hi : ℚ and valid : lo ≤ hi, as defined in Numerics.Interval.Basic and mirrored in Recognition.Certification. This definition supplies one concrete enclosure for the fifth power of π.
proof idea
The definition constructs the Interval record by direct assignment of the rational constants 305 and 312, then discharges the validity proof obligation with the norm_num tactic.
why it matters
The interval is the concrete enclosure consumed by the downstream theorem pi_pow5_in_interval, which certifies containment of π^5. It supports the numerical layer required for Recognition Science constants whose values are expressed via powers of π, including the fine-structure constant whose inverse is constrained to the band (137.030, 137.039).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.