module module high

`IndisputableMonolith.Numerics.Interval.PiBounds`

This module supplies verified rational-endpoint intervals containing π to six decimal places of precision. Numerics work in the Recognition framework cites it when constructing bounds for trigonometric functions downstream. The module imports the Basic interval arithmetic layer and Mathlib's pi bounds to define the intervals and prove containment.

claimAn interval $I$ with rational endpoints $a < b$ such that $\pi \in I$ and $b - a < 10^{-6}$.

background

The upstream Basic module supplies verified interval arithmetic that uses rational endpoints to bound real values. This PiBounds module specializes those tools to π. The local setting is the numerics layer of Recognition Science, where exact bounds on constants support later interval computations for physical constants and functions.

proof idea

This is a definition module that constructs specific intervals (piInterval, fourPiInterval, piSqInterval) and proves containment using the imported pi bounds from Mathlib together with interval operations from Basic.

why it matters in Recognition Science

The module feeds the trigonometric interval computations in IndisputableMonolith.Numerics.Interval.Trig, which relies on these π bounds for arctan and tan intervals. It supports the constructive proofs in the Recognition framework's numerics layer.

scope and limits

Does not extend to arbitrary precision or other irrationals.
Does not include floating-point error analysis.
Does not compute bounds for e or other constants.

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