module module high

`IndisputableMonolith.Numerics.Interval.Basic`

This module defines the core type of closed intervals with rational endpoints to underpin rigorous numerical bounds throughout the Recognition Science numerics layer. Interval arithmetic developers for exponential, logarithmic, and constant bounds cite it as the shared foundation. It supplies the Interval structure plus basic operations such as addition, negation, and containment checks, with no proof content.

claimA closed interval $I = [q_1, q_2]$ where $q_1, q_2$ are rational numbers, equipped with operations for addition, negation, and point containment.

background

The Numerics.Interval.Basic module introduces the Interval type as a closed interval whose endpoints lie in the rationals. It supplies the basic constructors and predicates (contains, point, add, neg) that later modules rely on for sound interval arithmetic. These definitions sit inside the broader Numerics domain and are imported by every higher-level bound module.

proof idea

This is a definition module with no proofs; it simply declares the Interval data type and the elementary operations on it.

why it matters in Recognition Science

The module supplies the shared interval type consumed by all downstream interval-arithmetic modules (Exp, Log, PhiBounds, PiBounds, Pow, GalacticBounds). Those modules in turn deliver the rigorous bounds on φ, π, exp, and log that feed the Recognition Science mass ladder and constant calculations.

scope and limits

Does not implement floating-point or real-number endpoints.
Does not compute bounds for transcendental functions.
Does not include automatic error propagation or advanced tactics.
Does not handle open or half-open intervals.

used by (8)

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

IndisputableMonolith.Numerics.Interval.Exp module_import
IndisputableMonolith.Numerics.Interval.GalacticBounds module_import
IndisputableMonolith.Numerics.Interval.Log module_import
IndisputableMonolith.Numerics.Interval.PhiBounds module_import
IndisputableMonolith.Numerics.Interval.PiBounds module_import
IndisputableMonolith.Numerics.Interval.Pow module_import
IndisputableMonolith.Numerics.Interval.Tactic module_import
IndisputableMonolith.Numerics.Interval.Trig module_import

declarations in this module (27)

structure Interval L16
def contains L25
def point L29
theorem contains_point L34
def mk' L38
def add L46
theorem add_lo L54
theorem add_hi L55
theorem add_contains_add L57
def neg L66
theorem neg_lo L74
theorem neg_hi L75
theorem neg_contains_neg L77
def sub L85
theorem sub_lo L93
theorem sub_hi L94
theorem sub_contains_sub L96
def mulPos L105
theorem mulPos_contains_mul L113
def smulPos L128
theorem smulPos_contains_smul L133
def npow L143
theorem npow_contains_pow L149
theorem lo_gt_implies_contains_gt L162
theorem hi_lt_implies_contains_lt L167
theorem lo_ge_implies_contains_ge L172
theorem hi_le_implies_contains_le L177