LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

Continuous second partials of a scalar potential commute

Statement

Let $U \subseteq R^{n}$ be open and let $ϕ : U \to R$ have continuous second partial derivatives. Then

$\partial_{j} \partial_{i} ϕ (x) = \partial_{i} \partial_{j} ϕ (x)$

for every $x \in U$ and every pair of coordinate indices $i, j$ .

Facts & Assumptions

Given: The open set, function, point, and indices in the Statement.

[L1]

The coordinate partial derivative $\partial_{i} ϕ (x)$ is the derivative at zero of $t \mapsto ϕ (x + t e_{i})$ (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ).

[L2]

A real function continuous on $[a, b]$ and differentiable on $(a, b)$ has an interior point $c$ with $f (b) - f (a) = f^{'} (c) (b - a)$ (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

Proof

technique · direct

1.1

If $i = j$ , the displayed equality has identical sides. Assume henceforth that $i \neq j$ . Since $U$ is open, choose a ball about $x$ contained in $U$ , and choose nonzero $h, k$ small enough that the coordinate rectangle with vertices $x$ , $x + h e_{i}$ , $x + k e_{j}$ , and $x + h e_{i} + k e_{j}$ lies in that ball.

givencases

2.1

Divide the rectangular difference $R (h, k) : = ϕ (x + h e_{i} + k e_{j}) - ϕ (x + h e_{i}) - ϕ (x + k e_{j}) + ϕ (x)$ by $h k$ . Apply [L2] on the ordered endpoint intervals first in direction $i$ and then in direction $j$ ; this covers either sign of $h$ and $k$ . Using [L1], there are points $ξ$ and $η$ inside the corresponding coordinate intervals such that $\frac{R (h, k)}{h k} = \partial_{j} \partial_{i} ϕ (x + ξ e_{i} + η e_{j}) .$

step 1.1L1L2algebra

2.2

Applying [L2] in the opposite order gives interior points $ξ^{'}$ and $η^{'}$ such that the same quotient equals $\frac{R (h, k)}{h k} = \partial_{i} \partial_{j} ϕ (x + ξ^{'} e_{i} + η^{'} e_{j}) .$

step 1.1L1L2algebra

3.1

Let $h$ and $k$ tend to zero through nonzero values. All four intermediate displacements tend to zero. Continuity of the two second partials in steps 2.1 and 2.2 therefore gives $\partial_{j} \partial_{i} ϕ (x) = \partial_{i} \partial_{j} ϕ (x) .$

step 2.1step 2.2given

4.1

Together with the $i = j$ case in step 1.1, this proves the assertion for every pair of indices.

step 1.1step 3.1∎

Depends on

Used by

Every exact C1 vector field is closed Theorem

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 71 results over 18 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

J.-B. Campesato, Poincare Lemma, section 1 (standard reference, not scraped)