pith. machine review for the scientific record. sign in
module module high

IndisputableMonolith.Numerics.Interval.Basic

show as:
view Lean formalization →

The basic interval module defines a closed interval whose endpoints are rational numbers, together with addition, negation, and a containment predicate. Developers building rigorous bounds on transcendental and algebraic constants inside Recognition Science import it to keep every numeric estimate exact and machine-verifiable. The module supplies only the core type and elementary operations; no deep proofs are present.

claimLet $I=[q_1,q_2]$ be a closed interval with rational endpoints $q_1,q_2$ satisfying $q_1leq q_2$. The module supplies the corresponding type, the predicate that a real number lies inside $I$, and the interval versions of addition and negation.

background

This module sits at the root of the Numerics.Interval hierarchy and supplies the data type used by every higher-level bound. An interval is represented by a pair of rationals that serve as exact lower and upper bounds, guaranteeing that all arithmetic remains inside Lean without approximation. The contains predicate tests membership of a real point, while mk' constructs an interval from two rationals and add, neg preserve the containment relation.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

It supplies the common interval substrate required by the exponential, logarithmic, power, phi-bounds, and pi-bounds modules. Those modules deliver the verified estimates that underwrite the Recognition Science constants (c=1, hbar=phi^{-5}, G=phi^5/pi) and the mass ladder on the phi-ladder. Without this foundation the entire numeric verification layer would lack an exact, shared substrate.

scope and limits

used by (8)

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

declarations in this module (27)