LemmaStatement: AI-adaptedProof: 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.

Potentials glue after a constant adjustment over a nonempty path-connected overlap

Statement

Let $U_{1}, U_{2} \subseteq R^{n}$ be open, with nonempty piecewise- $C^{1}$ path-connected intersection. Suppose $F : U_{1} \cup U_{2} \to R^{n}$ has $C^{1}$ potentials $ϕ_{i}$ on $U_{i}$ . Then there is a constant $C$ such that

$ϕ (x) : = {\begin{cases} ϕ_{1} (x), & x \in U_{1}, \\ ϕ_{2} (x) + C, & x \in U_{2} . \end{cases}$

is a well-defined $C^{1}$ potential for $F$ on $U_{1} \cup U_{2}$ .

Facts & Assumptions

Given: The two open sets, field, potentials, and overlap in the Statement.

[L1]

Two potentials of the same field differ by a constant on each piecewise- $C^{1}$ path component of their common domain (Two potentials of the same field differ by a constant on each piecewise-C1 path component).

Proof

technique · direct

1.1

On $U_{1} \cap U_{2}$ , both gradients equal $F$ . Since this intersection is nonempty and piecewise- $C^{1}$ path-connected, [L1] gives a single constant $C$ such that $ϕ_{1} - ϕ_{2} = C$ throughout the overlap.

givenL1

2.1

Therefore the two clauses in the displayed definition of $ϕ$ agree at every point of $U_{1} \cap U_{2}$ , so $ϕ$ is well-defined.

step 1.1algebra

3.1

Every point of $U_{1} \cup U_{2}$ has a neighbourhood on which $ϕ$ equals either the $C^{1}$ function $ϕ_{1}$ or the $C^{1}$ function $ϕ_{2} + C$ . Hence $ϕ$ is $C^{1}$ on the union.

givenstep 2.1

4.1

On those same neighbourhoods, $\nabla ϕ$ equals $\nabla ϕ_{1} = F$ or $\nabla (ϕ_{2} + C) = F$ . Thus $\nabla ϕ = F$ on all of $U_{1} \cup U_{2}$ .

givenstep 3.1algebra

5.1

Steps 2.1, 3.1, and 4.1 prove the gluing assertion. Nonemptiness permits a comparison constant, and path-connectedness makes one adjustment valid on the whole overlap.

step 2.1step 3.1step 4.1∎

Depends on

Two potentials of the same field differ by a constant on each piecewise-C1 path component

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 18 results over 7 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. Lebl, Basic Analysis II, section 9.3 (standard reference, not scraped)