Certified inequality checks and adaptive subdivision

Rational input boxes denote sets of arbitrary real assignments. Endpoint enclosure preserves these sets, and backend soundness carries their values through expression evaluation. A successful upper-bound test therefore proves the requested inequality throughout a box.

Every midpoint split covers its parent. Induction on the subdivision depth combines successful checks of both children without assuming that any sampled point represents the entire box.

def FloatLib.Numerics.Interval.Relation.Holds (relation : Relation) (value : ℝ) : Prop

Real meaning of the two relations accepted by the executable checker.

def FloatLib.Numerics.Interval.Box.ContainsReal (box : Box) (values : ℕ → ℝ) : Prop

A real assignment respects every supplied rational coordinate interval.

@[simp]

theorem FloatLib.Numerics.Interval.Box.containsReal_nil (values : ℕ → ℝ) : ContainsReal [] values

An empty box places no restrictions on the real environment.

@[simp]

theorem FloatLib.Numerics.Interval.Box.containsReal_cons_iff (I : Interval ℚ) (box : Box) (values : ℕ → ℝ) : ContainsReal (I :: box) values ↔ (↑I.lo ≤ values 0 ∧ values 0 ≤ ↑I.hi) ∧ box.ContainsReal fun (i : ℕ) => values (i + 1)

Separate the first coordinate's bounds from the shifted tail environment.

theorem FloatLib.Numerics.Interval.Box.containsReal_cons {I : Interval ℚ} {box : Box} {values : ℕ → ℝ} (head : ↑I.lo ≤ values 0 ∧ values 0 ≤ ↑I.hi) (tail : box.ContainsReal fun (i : ℕ) => values (i + 1)) : ContainsReal (I :: box) values

Build box membership one coordinate at a time from real bounds.

theorem FloatLib.Numerics.Interval.Backend.containsReal_encloseInterval? {functions : ℕ → List ℝ → ℝ} {α : Type u_1} {B : Backend α} (hB : B.Sound functions) {I : Interval ℚ} {J : Interval α} (h : B.encloseInterval? I = some J) {x : ℝ} (hx : ContainsReal some I x) : ContainsReal B.decode J x

Enclosing rational endpoints contains every real between them.

theorem FloatLib.Numerics.Interval.Box.containsReal_enclose? {functions : ℕ → List ℝ → ℝ} {α : Type u_1} {B : Backend α} (hB : B.Sound functions) {box : Box} {intervals : List (Interval α)} (h : box.enclose? B = some intervals) {values : ℕ → ℝ} (hbox : box.ContainsReal values) (i : ℕ) (I : Interval α) : intervals[i]? = some I → Interval.ContainsReal B.decode I (values i)

Successful box enclosure supplies sound values for every coordinate in the interval list.

theorem FloatLib.Numerics.Interval.Relation.holds_of_check {relation : Relation} {hi : ℚ} (h : relation.check hi = true) {x : ℝ} (hx : x ≤ ↑hi) : relation.Holds x

A checked upper bound implies the corresponding relation for every smaller real number.

theorem FloatLib.Numerics.Interval.Expr.checkBox_sound {functions : ℕ → List ℝ → ℝ} {α : Type u_1} (e : Expr) {B : Backend α} (hB : B.Sound functions) {relation : Relation} {box : Box} (h : e.checkBox B relation box = true) {values : ℕ → ℝ} (hbox : box.ContainsReal values) : relation.Holds (e.eval values functions)

A successful leaf check establishes the inequality for every real assignment in its box.

theorem FloatLib.Numerics.Interval.Box.containsReal_set {box : Box} {values : ℕ → ℝ} (hbox : box.ContainsReal values) {i : ℕ} {I : Interval ℚ} (hI : Interval.ContainsReal some I (values i)) : ContainsReal (List.set box i I) values

Replacing a coordinate preserves membership when the new interval contains its value.

theorem FloatLib.Numerics.Interval.Box.containsReal_bisect? {box left right : Box} (h : box.bisect? = some (left, right)) {values : ℕ → ℝ} (hbox : box.ContainsReal values) : left.ContainsReal values ∨ right.ContainsReal values

Every real assignment in a split box belongs to at least one of its two children.

theorem FloatLib.Numerics.Interval.Expr.check_sound {functions : ℕ → List ℝ → ℝ} {α : Type u_1} (e : Expr) {B : Backend α} (hB : B.Sound functions) {relation : Relation} {box : Box} {depth : ℕ} (h : e.check B relation box depth = true) {values : ℕ → ℝ} (hbox : box.ContainsReal values) : relation.Holds (e.eval values functions)

A successful adaptive check proves the real inequality throughout the original rational box.

The computation depends only on the backend, expression, rational box, relation, and depth. The real environment and its membership proof enter only this theorem.