TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Scalar interval Newton exclusion and strict inclusion certificates

Statement

Let $f$ be $C^{1}$ on an open interval containing $X = [a, b]$ , with $a < b$ . Let $F_{m}$ enclose $f (m)$ , let $D$ enclose $f^{'} (X)$ with $0 \notin D$ , and let $N = m - F_{m} / D$ be the finite outward interval Newton image, where $m = (a + b) / 2$ . Every root of $f$ in $X$ belongs to $N \cap X$ . Consequently, $0 \notin E_{f} (X)$ for a valid range enclosure $E_{f} (X)$ , or $N \cap X = \emptyset$ , certifies that $X$ has no root. If $N \subset int X$ , then $f$ has exactly one root in $X$ . When the finite update budget ends without one of these certificates, the algorithm returns "inconclusive" and proves no absence claim.

Facts & Assumptions

Given: The input enclosures and interval Newton image from Finite-budget scalar interval Newton root certification, with interval operations as defined in Outward-rounded interval, rectangle and ball operations.

[F1]

Every finite real interval operation encloses its exact operation range (Finite real interval operations enclose their exact values).

[F2]

A continuous function on a closed interval, differentiable in its interior, satisfies the mean value theorem (Mean value theorem on a closed real interval).

[F3]

A continuous function takes every intermediate value between its endpoint values (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ ).

[F4]

A real-interval $C^{1}$ function is continuous on its interval and has the stated continuous derivative (Continuity and derivative on a real interval).

[F5]

The scalar procedure preserves the root set when it replaces an interval $I$ by $N (I) \cap I$ , returns "unique-root" at a singleton only when its exact range enclosure is ${0}$ , and returns "inconclusive" on an exhausted update budget (Finite-budget scalar interval Newton root certification).

Proof

1.1givenF1F2algebra

If $r \in X$ is a root and $r = m$ , then $0 = f (m) \in F_{m}$ , so $m \in N$ . If $r \neq m$ , the mean value theorem on the segment between $m$ and $r$ gives $ξ \in X$ with $f (m) = f^{'} (ξ) (m - r)$ . Since $f^{'} (ξ) \in D$ and $f (m) \in F_{m}$ , interval enclosure [F1] gives $r = m - f (m) / f^{'} (ξ) \in N$ . Hence every root in $X$ lies in $N \cap X$ , and an empty intersection excludes all roots.

1.2givenF1algebra

If $0 \notin E_{f} (X)$ and the range enclosure is valid, no $x \in X$ can satisfy $f (x) = 0$ , because $f (X) \subseteq E_{f} (X)$ .

1.3givenF1F2F4choose

Suppose $N \subset int X$ . Since $0 \notin D$ and $D$ is an interval, every value of $f^{'}$ on $X$ has one fixed strict sign. Let $ξ_{a} \in (a, m)$ and $ξ_{b} \in (m, b)$ be the mean-value points for $[a, m]$ and $[m, b]$ , and put $d_{a} = f^{'} (ξ_{a})$ and $d_{b} = f^{'} (ξ_{b})$ . The exact Newton points $n_{a} = m - f (m) / d_{a}$ and $n_{b} = m - f (m) / d_{b}$ lie in $N$ , so $a < n_{a}$ and $n_{b} < b$ .

2.1givenF1F5step 1.1induction

At each strict interval update, every root of the current interval belongs to $N \cap I$ by step 1.1, so induction shows that no root of the original box is lost. If the current interval is a singleton ${x}$ and the algorithm returns "unique-root", then $E_{f} ({x}) = {0}$ implies $f (x) = 0$ ; root preservation shows this is the only root of the original box.

2.2step 1.3F3algebra

If $d_{a}, d_{b} > 0$ , the inequality $a < n_{a}$ gives $f (a) = f (m) - d_{a} (m - a) < 0$ , and $n_{b} < b$ gives $f (b) = f (m) + d_{b} (b - m) > 0$ . If $d_{a}, d_{b} < 0$ , multiplying the same inequalities by the negative derivatives reverses them and gives $f (a) > 0 > f (b)$ . In either case [F3] supplies a root in $(a, b)$ .

3.1givenF2step 2.2F4algebra

For any $x < y$ in $X$ , [F2] gives $f (y) - f (x) = f^{'} (ζ) (y - x)$ for some $ζ \in (x, y)$ . The derivative has the same strict sign throughout $X$ , so $f$ is strictly monotone there and has at most one root. Together with step 2.2, the root is unique.

4.1givenF5∎

If no exclusion or strict-inclusion test succeeds before the update budget ends, the algorithm's final branch returns "inconclusive" by [F5]; this branch supplies no root-absence conclusion.

Depends on

Used by

Cited to discharge well-definedness by Finite-budget scalar interval Newton root certification.

Dependency tree · two levels

29 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Siegfried M. Rump, Verification methods: Rigorous results using floating-point arithmetic, Acta Numerica 19 (2010), Theorem 6.2 (standard reference, not scraped)
R. Baker Kearfott, Interval Computations: Introduction, Uses, and Resources, Theorem 2 (standard reference, not scraped)