LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

An interval Jacobian encloses a vector mean-value matrix

Statement

Let $U \subseteq R^{n}$ be open and convex, let $X \subset U$ be a real box, and let $F : U \to R^{n}$ be $C^{1}$ . Let $J (X)$ be an interval Jacobian enclosure. For any $x, y \in X$ , there is a point matrix $A \in J (X)$ such that

F (x) - F (y) = A (x - y) .

The rows of $A$ may come from different intermediate points; the claim does not assert one common Jacobian value.

Facts & Assumptions

Given: $U, X, F, J (X), x, y$ as in the Statement.

[F1]

A $C^{1}$ map is totally differentiable on its open domain (Continuously differentiable maps, local inverses, and local diffeomorphisms), and total differentiability gives continuity (Total differentiability gives a local $O (∥ h ∥_{2})$ increment bound and therefore continuity).

[F2]

The chain rule computes the derivative of a composition with an affine line (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ ).

[F3]

A total derivative computes directional derivatives, and its matrix is the Jacobian (A total derivative computes every directional derivative, and its matrix is the Jacobian).

[F4]

A real function continuous on $[a, b]$ and differentiable on $(a, b)$ satisfies the mean value theorem (Mean value theorem on a closed real interval).

[F5]

Each interval-Jacobian entry contains the corresponding partial derivative at every point of $X$ (Real boxes and interval Jacobian enclosures).

Proof

1.1givenF1F2F3construct

Use coordinate indices $0 \leq i, j < n$ , as for the Jacobian. Fix a row index $i$ and define $ϕ_{i} (t) = F_{i} (y + t (x - y))$ on $[0, 1]$ . For $0 \leq t \leq 1$ and every coordinate $j$ , both $x_{j}, y_{j} \in [a_{j}, b_{j}]$ imply $(1 - t) y_{j} + t x_{j} \in [a_{j}, b_{j}]$ . Thus the product box $X$ is convex and the segment stays in $X \subset U$ . By [F1], $F_{i}$ is continuous there; by [F2] and [F3], $ϕ_{i}$ is differentiable on $(0, 1)$ with $ϕ_{i}^{'} (t) = \sum_{j = 0}^{n - 1} \partial_{j} F_{i} (y + t (x - y)) (x_{j} - y_{j})$ .

2.1step 1.1F4construct

Apply [F4] to $ϕ_{i}$ to obtain $t_{i} \in (0, 1)$ with $F_{i} (x) - F_{i} (y) = \sum_{j = 0}^{n - 1} \partial_{j} F_{i} (z_{i}) (x_{j} - y_{j})$ , where $z_{i} = y + t_{i} (x - y) \in X$ .

3.1step 2.1F5choosealgebra∎

For each of the finitely many rows choose the point $z_{i}$ from step 2.1 and form $A$ whose $i$ th row is $\nabla F_{i} (z_{i})$ . By [F5], every entry $A_{i j}$ lies in $J_{i j} (X)$ , so $A \in J (X)$ ; the row identities in step 2.1 give $F (x) - F (y) = A (x - y)$ . This uses only finite choice.

Depends on

Used by

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

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), Theorem 13.1 (standard reference, not scraped)
R. Baker Kearfott, Interval Computations: Introduction, Uses, and Resources, §2 (standard reference, not scraped)