module module high

`IndisputableMonolith.Numerics.Interval.PiBounds`

The PiBounds module supplies rational-endpoint intervals containing π to six decimal places. Workers on constructive trigonometry bounds cite these intervals to anchor arctan and tan estimates. The module assembles the bounds by importing the verified interval arithmetic primitives and applying them to known rational approximations of π.

claimThe module defines an interval $I$ with rational endpoints such that $3.141592 < I < 3.141593$ (width less than $10^{-6}$), together with the derived intervals for $4π$ and $π^2$ satisfying the same precision.

background

The module sits inside the verified interval arithmetic framework of the Basic module. That module states: 'This module provides rigorous interval arithmetic for computing bounds on transcendental functions. The key insight is that we use rational endpoints (which Lean can compute exactly) to bound real values.' All endpoints remain rational so that Lean can decide containment exactly without floating-point error.

proof idea

This module consists of definitions for the interval objects together with containment theorems. Each bound is obtained by applying the interval operations imported from Basic to explicit rational approximations of π; no single top-level proof exists.

why it matters in Recognition Science

This module supplies the π intervals required by the Trig module for its constructive arctan and tan bounds. The downstream module states that all arctan bounds are proved constructively using derivative-comparison monotonicity, so the six-decimal π anchors serve as the base constants in that layer.

scope and limits

Does not supply intervals for constants other than π, 4π and π².
Does not achieve precision finer than six decimal places.
Does not implement general interval arithmetic beyond the listed siblings.
Does not prove bounds for composite expressions involving π.

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