piPow5IntervalTight
plain-language theorem explainer
This definition supplies the narrow rational interval [306.0193, 306.0199] guaranteed to contain π^5. Numerics researchers in Recognition Science cite it when they require machine-checkable bounds on powers of π for interval arithmetic. The construction is a direct record definition whose validity obligation is discharged by norm_num.
Claim. Let $I$ be the closed interval with rational endpoints $3060193/10000$ and $3060199/10000$. Then $I$ satisfies the interval validity condition that the lower endpoint is at most the upper endpoint.
background
The module supplies rigorous bounds on π by importing Mathlib's proven inequalities such as π > 3.141592. The Interval structure is defined as a record with rational fields lo and hi together with a proof that lo ≤ hi. This definition specializes that structure to a tight enclosure around π^5.
proof idea
The definition constructs the Interval record directly by assigning the lower endpoint 3060193/10000, the upper endpoint 3060199/10000, and discharging the lo ≤ hi obligation with the norm_num tactic.
why it matters
The interval is consumed by the downstream theorem pi_pow5_in_interval_tight, which proves π^5 lies inside it. It supports the numerics layer by providing certified rational bounds that can be used in further interval computations involving powers of π.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.