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

Interval

show as:
view Lean formalization →

Interval structures appear throughout Recognition.Certification to represent bounded real quantities with explicit endpoint ordering. Physicists modeling measurement uncertainty or musicians analyzing harmonic intervals reference this structure when they need to certify that a value lies between two reals. It is introduced as a plain structure definition with three fields: the lower bound, upper bound, and the ordering proof. The definition mirrors the rational-endpoint version from Numerics.Interval.Basic but lifts the endpoints to reals.

claimA closed interval on the reals is a triple $(lo, hi, lo_le_hi)$ where $lo, hi : ℝ$ and $lo ≤ hi$.

background

The Recognition.Certification module imports the basic interval structure from Numerics.Interval.Basic, which defines intervals over rationals with a validity predicate. This real-valued version replaces the rational endpoints with reals while retaining the lo ≤ hi constraint. It serves as a lightweight container for interval bounds in contexts such as uncertainty reporting and scale certifications.

proof idea

This is a structure definition, so the declaration itself constructs the type with the three fields without additional lemmas or tactics.

why it matters in Recognition Science

This structure is used in forty downstream declarations, including uncertainty semantics in Measurement.RSNative.Core (which includes an interval constructor), BCS ratio approximations in Chemistry.SuperconductingTc, and musical scale commas in Aesthetics.MusicalScale. It provides the interval representation needed for bounded-quantity certification without invoking full probability measures.

scope and limits

formal statement (Lean)

  11structure Interval where
  12  lo : ℝ
  13  hi : ℝ
  14  lo_le_hi : lo ≤ hi
  15

used by (40)

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

… and 10 more

depends on (1)

Lean names referenced from this declaration's body.