module module high

`IndisputableMonolith.Numerics.Interval.PiBounds`

This module supplies verified rational-endpoint intervals containing π accurate to six decimal places. Researchers needing constructive bounds for trigonometric functions cite it to maintain exactness in Lean. It consists of interval definitions and membership theorems built on the basic interval arithmetic module.

claimAn interval $I$ with rational endpoints such that $\pi \in I$ and the width of $I$ is less than $10^{-6}$, together with similar intervals for $4\pi$ and $\pi^2$.

background

The module sits in the Numerics domain and imports the Basic interval module, whose doc-comment states that rational endpoints allow Lean to compute exact bounds on real values. This supplies the setting for handling transcendental constants without floating-point approximations.

The module declares specific intervals for π and its multiples, then proves containment. These objects feed directly into trigonometric interval work that relies on derivative monotonicity for constructive proofs.

proof idea

The module declares interval objects for π, 4π, and π² then proves membership via the imported interval operations; no complex tactic sequences are required beyond the basic arithmetic already verified upstream.

why it matters in Recognition Science

This module feeds the Trig module, whose doc-comment describes constructive arctan bounds via derivative-comparison monotonicity. It supplies the required π constant bounds inside the Recognition Science numerics framework for rigorous transcendental function arithmetic.

scope and limits

Does not extend precision beyond six decimal places.
Does not provide bounds for constants other than π and its multiples.
Does not include complex or higher-dimensional interval arithmetic.

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

IndisputableMonolith.Numerics.Interval.Trig module_import

depends on (1)

Lean names referenced from this declaration's body.

IndisputableMonolith.Numerics.Interval.Basic module_import

declarations in this module (25)

def piInterval L32
theorem pi_in_piInterval L38
def piIntervalWide L55
theorem pi_in_piIntervalWide L61
theorem four_pi_gt L78
theorem four_pi_lt L83
def fourPiInterval L88
theorem four_pi_in_interval L94
theorem pi_sq_gt L107
theorem pi_sq_lt L115
def piSqInterval L123
theorem pi_sq_in_interval L129
theorem pi_pow5_eq L142
theorem pi_pow5_gt L145
theorem pi_pow5_lt L158
def piPow5Interval L170
theorem pi_pow5_in_interval L176
theorem four_pi_gt_d6 L189
theorem four_pi_lt_d6 L194
def fourPiIntervalTight L199
theorem four_pi_in_interval_tight L205
theorem pi_pow5_gt_d6 L216
theorem pi_pow5_lt_d6 L228
def piPow5IntervalTight L239
theorem pi_pow5_in_interval_tight L245