module module high

`IndisputableMonolith.Numerics.Interval.PiBounds`

This module supplies verified rational-endpoint intervals containing π to six decimal places of precision, together with companion intervals for 4π and π². Numerics work in Recognition Science cites these intervals when constructing rigorous bounds for trigonometric functions. The module assembles the intervals from Mathlib's pi bounds and proves containment via the interval arithmetic primitives imported from Basic.

claimThe module defines an interval $I_π$ with rational endpoints such that $π ∈ I_π$ and the width of $I_π$ is less than $10^{-6}$, together with analogous intervals $I_{4π}$ and $I_{π²}$ satisfying $4π ∈ I_{4π}$ and $π² ∈ I_{π²}$.

background

The module sits inside the Numerics domain and imports verified interval arithmetic from IndisputableMonolith.Numerics.Interval.Basic. That upstream module supplies the core operations that bound real numbers by intervals whose endpoints are rational, allowing exact Lean computation. It also imports Mathlib.Analysis.Real.Pi.Bounds to obtain concrete starting approximations for π.

proof idea

The module is a collection of interval definitions (piInterval, fourPiInterval, piSqInterval) paired with containment theorems (pi_in_piInterval, four_pi_in_interval, pi_sq_in_interval). Each containment is established by applying the interval operations defined in Basic to the pi bounds supplied by Mathlib.

why it matters in Recognition Science

The intervals are consumed by the trigonometric module IndisputableMonolith.Numerics.Interval.Trig, which uses them to obtain rigorous bounds on arctan and tan. This placement supplies the constant-precision layer required for the constructive derivative-comparison proofs that appear downstream.

scope and limits

Does not derive π bounds from first principles inside Recognition Science.
Does not support arbitrary-precision or adaptive-precision intervals.
Does not contain bounds for other transcendental constants such as e.
Does not prove any statements about the Recognition forcing chain or J-function.

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