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.

Krawczyk inclusion proves existence, disjointness excludes roots, and contraction proves uniqueness

Statement

Let $U \subseteq R^{n}$ be open and convex, let $X \subset U$ be a nonempty real box, and let $F : U \to R^{n}$ be $C^{1}$ . For a processed box $Y \subseteq X$ , let $x_{0} \in Y$ , let $C$ be a nonsingular point matrix, let $F_{0}$ enclose $F (x_{0})$ , and let $J (Y)$ enclose every Jacobian entry on $Y$ . Form the outward interval box

K = x_{0} - C F_{0} + (I - C J (Y)) (Y - x_{0}) .

Every root of $F$ in $Y$ lies in $K$ . Thus $K \cap Y = \emptyset$ proves that $Y$ has no root. If $K \subset int Y$ , then $F$ has at least one root in $Y$ . Define $∥ v ∥_{\infty} = \max_{i} ∣ v_{i} ∣$ and $∥ A ∥_{\infty} = \max_{i} \sum_{j} ∣ A_{i j} ∣$ . Let $E$ be the outward interval matrix enclosing $I - C J (Y)$ and put $\overset{ˉ}{q} = \max_{i} \sum_{j} \max (∣ \inf E_{i j} ∣, ∣ \sup E_{i j} ∣)$ . If $\overset{ˉ}{q} < 1$ , then $F$ has at most one root in $Y$ ; strict inclusion together with this bound proves a unique root. No uniqueness is inferred from strict inclusion alone.

For a run with a verified nonsingular preconditioner and valid interval evaluators, every finite execution of Finite-budget multidimensional Krawczyk root certification terminates, and each root in the initial box lies in a unique-root, existence-only, or unresolved output box. Root-free outputs contain no root; unique-root outputs contain exactly one; an existence-only output proves at least one but makes no count claim. An unresolved or existence-only output prevents an all-roots conclusion.

Facts & Assumptions

Given: $F, U, X, Y, x_{0}, C, F_{0}, J (Y)$ and the Krawczyk box in the Statement.

[F1]

Every continuous self-map of a nonempty closed real box has a fixed point (A continuous self-map of a nonempty closed box has a fixed point).

[F2]

For any $x, y \in Y$ , there is a rowwise mean-value matrix $A \in J (Y)$ with $F (x) - F (y) = A (x - y)$ (An interval Jacobian encloses a vector mean-value matrix).

[F3]

Finite real interval operations enclose their exact values and finite expression evaluations (Finite real interval operations enclose their exact values).

[F4]

A $C^{1}$ map is continuous on its open domain (Total differentiability gives a local $O (∥ h ∥_{2})$ increment bound and therefore continuity).

[F5]

The Krawczyk algorithm checks an exact left-inverse witness for $C$ , computes $K$ and $E = I - C J (Y)$ by outward operations, and returns "unique-root" only when strict inclusion and $\overset{ˉ}{q} < 1$ both hold (Finite-budget multidimensional Krawczyk root certification).

[F6]

The real box, its interior, and the interval Jacobian set $J (X)$ have the definitions used here (Real boxes and interval Jacobian enclosures).

Proof

1.1givenF2F3F6algebrachoose

Fix a root $z \in Y$ . By [F2], choose $A \in J (Y)$ with $F (z) - F (x_{0}) = A (z - x_{0})$ . Since $F (z) = 0$ , rearrangement gives $z = x_{0} - C F (x_{0}) + (I - C A) (z - x_{0})$ . The enclosure conditions on $F_{0}, J (Y)$ and the finite interval operations [F3] place this exact value in $K$ .

2.1step 1.1algebra

Thus any root in $Y$ belongs to $K \cap Y$ ; if that intersection is empty, no root lies in $Y$ .

2.2givenF1F2F3F4F6step 1.1algebra

Define $g : Y \to R^{n}$ by $g (x) = x - C F (x)$ . It is continuous by [F4]. For every $x \in Y$ , [F2] applied to $x$ and $x_{0}$ gives a matrix in $J (Y)$ , and the same enclosure argument as in step 1.1 gives $g (x) \in K$ . If $K \subset int Y$ , then $g (Y) \subseteq Y$ ; [F1] gives $x \in Y$ with $g (x) = x$ . Since $C$ is nonsingular, this identity implies $F (x) = 0$ .

2.3givenF2F3step 1.1algebra

Suppose $x, y \in Y$ are both roots. Choose $A \in J (Y)$ from [F2]. By [F3], every entry of $I - C A$ lies in the corresponding interval $E_{i j}$ , so $∣ (I - C A)_{i j} ∣ \leq \max (∣ \inf E_{i j} ∣, ∣ \sup E_{i j} ∣)$ and $∥ I - C A ∥_{\infty} \leq \overset{ˉ}{q}$ . The rowwise identity gives $F (x) - F (y) = A (x - y) = 0$ , so $(I - C A) (x - y) = x - y$ . The row-sum definition of the induced infinity norm gives $∥ (I - C A) (x - y) ∥_{\infty} \leq \overset{ˉ}{q} ∥ x - y ∥_{\infty}$ . Since $\overset{ˉ}{q} < 1$ , $x = y$ .

3.1step 2.1step 2.2step 2.3F5

Strict inclusion supplies existence by step 2.2, and the certified contraction bound supplies at most one root by step 2.3. Thus "unique-root" is sound only in this combined case; with strict inclusion but no contraction bound, the algorithm reports "existence-only" by [F5]. Root-free output is justified by step 2.1, and unresolved output makes no claim.

4.1step 3.1F5inductionconstruct∎

The algorithm processes at most the finite budget $B$ . A non-finite evaluation marks its current box unresolved and leaves the remaining queue to be processed; every other inconclusive box is either marked unresolved or replaced by two closed halves whose union is the parent. Thus the bisection and queue rules preserve coverage of the initial box. Together with the sound terminal statuses in step 3.1, this proves that every initial root lies in a unique-root, existence-only, or unresolved output box. If an existence-only or unresolved box remains, no all-roots conclusion is made.

Depends on

Used by

A Krawczyk inclusion certifies a unique phase-fixed nonconstant periodic orbit Theorem

Cited to discharge well-definedness by Finite-budget multidimensional Krawczyk root certification.

Dependency tree · two levels

23 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), §13, Theorem 13.3, pp. 89–90 (standard reference, not scraped)
R. Baker Kearfott, Interval Computations: Introduction, Uses, and Resources, §2 (standard reference, not scraped)