pith. machine review for the scientific record. sign in
structure definition def or abbrev high

Interval

show as:
view Lean formalization →

Interval arithmetic here supplies a closed interval type with rational endpoints lo and hi obeying lo ≤ hi. Numerics modules and downstream results on bounds for phi-logarithms or BCS ratios cite it to obtain exact computable enclosures of real values. The declaration is a direct structure definition that derives decidable equality from the endpoint inequality.

claimA closed interval $[a,b]$ with $a,b$ rational and $a≤b$.

background

The module supplies verified interval arithmetic that bounds transcendental functions by rational endpoints, which Lean evaluates exactly. The structure Interval packages a lower bound lo : ℚ, upper bound hi : ℚ, and the proof obligation valid : lo ≤ hi. It is the rational-endpoint counterpart to the real-endpoint Interval declared in Recognition.Certification.

proof idea

Structure definition that introduces the three fields and attaches the DecidableEq instance; no tactics or lemmas are applied.

why it matters in Recognition Science

This definition supplies the basic numeric carrier used by bcs_ratio_approx (Chemistry.SuperconductingTc), comma_small (Aesthetics.MusicalScale), Uncertainty (Measurement.RSNative.Core), and several Navier-Stokes hypothesis interfaces. It therefore supports exact rational enclosures of constants such as log(φ) that appear in the phi-ladder and the alpha band. The structure closes the gap between abstract real analysis and machine-checkable bounds inside the Recognition framework.

scope and limits

formal statement (Lean)

  16structure Interval where
  17  lo : ℚ
  18  hi : ℚ
  19  valid : lo ≤ hi
  20  deriving DecidableEq
  21
  22namespace Interval
  23
  24/-- Containment: a real number x is in interval I if lo ≤ x ≤ hi -/

used by (40)

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

… and 10 more

depends on (6)

Lean names referenced from this declaration's body.