Interval
plain-language theorem explainer
Recognition.Certification supplies a structure for closed real intervals. Researchers handling measurement bounds, musical commas, or BCS ratios cite it when real endpoints must be packaged with an order witness. The definition is a direct structure declaration that lifts the rational-endpoint version from Numerics.Interval.Basic.
Claim. A closed interval on the reals consists of numbers $lo, hi$ satisfying $lo ≤ hi$.
background
Numerics.Interval.Basic.Interval supplies the identical structure but restricted to rational endpoints together with a decidable-equality derivation. Recognition.Certification lifts the construction to real numbers so that continuous quantities arising in certification can be bounded without rationality constraints. The module collects recognition-specific numeric primitives that feed interval-based statements in measurement, music theory, and chemistry.
proof idea
Direct structure definition introducing the three fields; no lemmas or tactics are invoked.
why it matters
The structure is referenced by forty downstream declarations, including the interval constructor inside Measurement.RSNative.Core.Uncertainty and the bound statements in MusicalScale.comma_small and SuperconductingTc.bcs_ratio_approx. It supplies the concrete interval type required once rational numerics are extended to real-valued recognition constants and phi-derived ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.