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

A closed 1-form on a simply connected open subset of the affine model has a primitive

Statement

Let $(A, V, η, C^{+})$ be an oriented time-oriented affine Minkowski space (Oriented time-oriented affine Minkowski space (the spacetime primitives)), let $U \subseteq A$ be a nonempty open subset which, with the topology of The affine atlas makes the Minkowski model a smooth 4-manifold diffeomorphic to R^4, is path-connected and simply connected (Simply connected topological spaces), and let $α$ be a $C^{1}$ one-form on $U$ with $d α = 0$ (Closed and exact differential forms); here closedness of a $C^{1}$ one-form means that in an inertial chart (Inertial frames and inertial charts of the affine Minkowski model) one has $α = \sum_{i = 0}^{3} a_{i} d x^{i}$ with $\partial_{i} a_{j} = \partial_{j} a_{i}$ , the exterior derivative being understood by this coefficient formula (The exterior derivative by the invariant vector-field formula, The local coordinate formula for the exterior derivative). Then:

(a) there is a $C^{2}$ function $F : U \to R$ with $d F = α$ ;

(b) for any two piecewise- $C^{1}$ paths $γ_{0}, γ_{1}$ in $U$ (Piecewise-C1 path-connected domains, potential functions, conservative fields, and path independence) with the same endpoints, the integrals of $α$ along them are equal, and consequently the integral of $α$ along every piecewise- $C^{1}$ loop in $U$ vanishes.

If $α$ is smooth, $F$ may be taken smooth.

Conventions (what the objects mean here). Fix one inertial chart $x : A \to R^{4}$ and put $Ω : = x (U) \subseteq R^{4}$ ; by The affine atlas makes the Minkowski model a smooth 4-manifold diffeomorphic to R^4 the chart $x$ is a diffeomorphism of $A$ onto $R^{4}$ carrying the model's topology, and every other inertial chart $x^{'}$ satisfies $x^{'} = M^{- 1} (x - b)$ for an invertible matrix $M$ and a vector $b$ . The $C^{1}$ one-form $α$ is represented in the chart as $α = \sum_{i = 0}^{3} a_{i} d x^{i}$ with coefficient functions $a_{i} : Ω \to R$ of class $C^{1}$ ; write $A : = (a_{0}, a_{1}, a_{2}, a_{3}) : Ω \to R^{4}$ for the coefficient field, so that $A$ is $C^{1}$ and closedness reads $\partial_{i} a_{j} = \partial_{j} a_{i}$ on $Ω$ . For a piecewise- $C^{1}$ path $γ$ in $U$ the integral is $\int_{γ} α : = \int_{x \circ γ} A \cdot d r$ , the vector-field line integral of Scalar line integrals with respect to arc length and vector-field line integrals. For a $C^{1}$ function $F : U \to R$ with $\tilde{F} : = F \circ x^{- 1}$ , the differential $d F$ is the one-form whose chart coefficients are the partial derivatives $\partial_{i} \tilde{F}$ , and $d F = α$ means $\partial_{i} \tilde{F} = a_{i}$ on $Ω$ for all $i$ . Under the transition $x^{'} = M^{- 1} (x - b)$ the chain rule gives $a_{j}^{'} = \sum_{i} M_{j}^{i} a_{i}$ , $\partial_{j} {\tilde{F}}^{'} = \sum_{i} M_{j}^{i} \partial_{i} \tilde{F}$ and $(x^{'} \circ γ)^{'} = M^{- 1} (x \circ γ)^{'}$ , so the integral $\int_{γ} α$ and the identity $d F = α$ do not depend on which inertial chart is used; likewise, $F$ being $C^{2}$ , respectively smooth, is chart-independent. It therefore suffices to prove the following statement about the open set $Ω \subseteq R^{4}$ and the $C^{1}$ closed field $A$ : every closed piecewise- $C^{1}$ path in $Ω$ has zero $A$ -integral, the $A$ -integral is path-independent on $Ω$ , and there is a $C^{2}$ function $\tilde{F}$ on $Ω$ with $\nabla \tilde{F} = A$ which can be taken smooth when $A$ is smooth.

Facts & Assumptions

Given: An oriented time-oriented affine Minkowski space $(A, V, η, C^{+})$ (Oriented time-oriented affine Minkowski space (the spacetime primitives)), a nonempty open subset $U \subseteq A$ that is path-connected and simply connected (Simply connected topological spaces) in the topology of The affine atlas makes the Minkowski model a smooth 4-manifold diffeomorphic to R^4, and a $C^{1}$ one-form $α$ on $U$ with $d α = 0$ in the coefficient sense of the Statement (Closed and exact differential forms, The exterior derivative by the invariant vector-field formula).

[F1]

An inertial chart $x : A \to R^{4}$ is a diffeomorphism of $A$ onto $R^{4}$ for the model's topology (which is independent of the chart), the transitions between inertial charts are the affine bijections $x^{'} = M^{- 1} (x - b)$ , and every inertial chart belongs to the same smooth structure (Inertial frames and inertial charts of the affine Minkowski model, The affine atlas makes the Minkowski model a smooth 4-manifold diffeomorphic to R^4, Oriented time-oriented affine Minkowski space (the spacetime primitives)).

[F2]

$U$ is nonempty and path-connected, and for every $u \in U$ the fundamental group $π_{1} (U, u)$ has exactly one element; equivalently, every based loop at $u$ is path-homotopic relative to the endpoints to the constant loop at $u$ (Simply connected topological spaces, Based loops and the fundamental group, Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints, Nullhomotopic maps and contractible spaces).

[F3]

A path homotopy relative to the endpoints from a loop $γ$ at $p$ to the constant loop is a continuous $H : I \times I \to U$ with $H (s, 0) = γ (s)$ , $H (s, 1) = p$ and $H (0, t) = H (1, t) = p$ , where $I = [0, 1]$ (Homotopies of continuous maps, homotopies relative to a subspace, and path homotopies relative to the endpoints).

[F4]

For a piecewise- $C^{1}$ path $γ : [a, b] \to R^{n}$ and a continuous field $F$ on a set containing its trace, $\int_{γ} F \cdot d r$ is the sum of the integrals of $⟨ F (γ (t)), v_{i} (t) ⟩$ over an admissible partition with continuous derivative extensions $v_{i}$ , the value being independent of the admissible partition (Scalar line integrals with respect to arc length and vector-field line integrals, The piecewise-C1 line-integral sums do not depend on the admissible partition, Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations).

[F5]

Reversal, concatenation and reparametrization: $\int_{γ^{-}} F \cdot d r = - \int_{γ} F \cdot d r$ ; if $α, β : [0, 1] \to R^{n}$ are piecewise- $C^{1}$ with $α (1) = β (0)$ then $\int_{α * β} F \cdot d r = \int_{α} F \cdot d r + \int_{β} F \cdot d r$ ; and an oriented piecewise- $C^{1}$ reparametrization with increasing derivative leaves the integral unchanged (Line integrals under reversal and concatenation, Scalar line integrals are parametrization-independent; vector line integrals retain orientation and change sign when it reverses, Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations).

[F6]

On an open star-shaped $W \subseteq R^{n}$ , a $C^{1}$ field $F : W \to R^{n}$ is closed if and only if it is exact, if and only if it is conservative, if and only if it is path-independent, if and only if the integral along every closed piecewise- $C^{1}$ path in $W$ vanishes; a conservative field is path-independent and has vanishing closed-path integrals; and for $C^{1}$ $φ : W \to R$ and piecewise- $C^{1}$ $γ$ in $W$ one has $\int_{γ} \nabla φ \cdot d r = φ (γ (end)) - φ (γ (start))$ (On a star-shaped open domain, closed, exact, conservative, path-independent, and zero-loop are equivalent, Conservative fields are path-independent and have zero integral around every closed path, The gradient theorem: the line integral of a gradient is the endpoint increment).

[F7]

Euclidean structure and compactness: $∣ z ∣_{2}$ and the distance $d_{2}$ on $R^{n}$ satisfy the triangle inequality and $∣ t z ∣_{2} = ∣ t ∣ ∣ z ∣_{2}$ , so every ball $B (z, r) = {y : ∣ y - z ∣_{2} < r}$ is convex; a continuous image of a compact space is compact (The image of a compact metric space under a continuous map is compact, and so is the image of any compact subset); a closed box ${y : a_{k} \leq y_{k} \leq b_{k}}$ in $R^{n}$ is compact, and a subset of $R^{n}$ is compact if and only if it is closed and bounded; a continuous map on a compact metric space is uniformly continuous (The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ , Each $∥ \cdot ∥_{p}$ is a norm on $R^{n}$ , and the induced metrics are exactly $d_{1}$ , $d_{2}$ and $d_{\infty}$ of the published metric-spaces page, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , Open cover, subcover, compact metric space, and compact subset of a metric space, A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous).

[F8]

For every real $ε > 0$ there is a natural number $m \geq 1$ with $1 / m < ε$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[F9]

Calculus: for totally differentiable maps $f : W \to Z \subseteq R^{n}$ , $g : Z \to R^{p}$ on open Euclidean domains, $D (g \circ f) (u) = D g (f (u)) \circ D f (u)$ ; a function whose first partial derivatives exist and are continuous is totally differentiable, so a function with continuous partial derivatives of order up to $k$ is $C^{k}$ in the sense of $C^{k}$ maps and multi-index derivative notation in Euclidean space; and the first fundamental theorem of calculus for continuous integrands (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative, $C^{k}$ maps and multi-index derivative notation in Euclidean space, The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive, The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set, Continuity of $f : A \to R$ at a point of $A$ and on $A$ : the $ε$ - $δ$ condition, its agreement with $\lim_{x \to c} f (x) = f (c)$ at a limit point, and continuity at an isolated point).

Proof

technique · direct

1.1F1F2F4F9given

Fix an inertial chart $x$ and put $Ω : = x (U)$ ; by [F1] the chart is a diffeomorphism onto $R^{4}$ , so $Ω$ is a nonempty open subset of $R^{4}$ , and because $x ∣_{U} : U \to Ω$ is a homeomorphism it induces a bijection between the continuous loops at $p$ in $U$ and those at $x (p)$ in $Ω$ and a bijection between homotopies relative to the endpoints of such loops (via composition with $x$ and $x^{- 1}$ ); hence $Ω$ is path-connected and $π_{1} (Ω, u)$ has exactly one element for every $u \in Ω$ by [F2]. Write $α = \sum_{i = 0}^{3} a_{i} d x^{i}$ in the chart with $C^{1}$ coefficients $a_{i}$ and $\partial_{i} a_{j} = \partial_{j} a_{i}$ , set $A : = (a_{0}, \dots, a_{3})$ , and recall from the conventions of the Statement that $\int_{γ} α = \int_{x \circ γ} A \cdot d r$ for piecewise- $C^{1}$ $γ$ , that $d F = α$ means $\partial_{i} \tilde{F} = a_{i}$ for $\tilde{F} = F \circ x^{- 1}$ , and that these interpretations are invariant under a change of inertial chart, by the transition formula $x^{'} = M^{- 1} (x - b)$ of [F1] together with the chain rule of [F9] applied to $a_{j}^{'} = \sum_{i} M_{j}^{i} a_{i}$ , $\partial_{j} {\tilde{F}}^{'} = \sum_{i} M_{j}^{i} \partial_{i} \tilde{F}$ and $(x^{'} \circ γ)^{'} = M^{- 1} (x \circ γ)^{'}$ ; consequently the Statement follows once it is proved for the open set $Ω$ and the $C^{1}$ closed field $A$ on it that (i) every closed piecewise- $C^{1}$ path in $Ω$ has zero $A$ -integral, (ii) the $A$ -integral is path-independent on $Ω$ , and (iii) there is a $C^{2}$ function on $Ω$ with gradient $A$ , smooth when $A$ is smooth.

2.1F6F7F9step 1.1

Local primitives on balls: let $B = B (z, ϱ) \subseteq Ω$ be an open Euclidean ball; it is convex by [F7], hence star-shaped, and $A ∣_{B}$ is a $C^{1}$ closed field on $B$ , so by [F6] there is a $C^{1}$ function $φ : B \to R$ with $\nabla φ = A ∣_{B}$ , and because $\partial_{j} φ = a_{j}$ is $C^{1}$ for every $j$ the function $φ$ is $C^{2}$ by [F9]. By the gradient theorem of [F6], every piecewise- $C^{1}$ path $η$ in $B$ satisfies $\int_{η} A \cdot d r = φ (η (end)) - φ (η (start))$ ; in particular the integral of $A$ along every closed piecewise- $C^{1}$ path in $B$ vanishes, and the integral along a piecewise- $C^{1}$ arc in $B$ depends only on the endpoints of the arc.

2.2F7F8step 1.1

Polygonal paths in $Ω$ : let $p, q \in Ω$ ; since $Ω$ is path-connected there is a continuous $c : [0, 1] \to Ω$ with $c (0) = p$ , $c (1) = q$ , and $K^{'} : = c ([0, 1])$ is compact by [F7]. Cover $K^{'}$ by the family of all balls $B (z, r)$ with $B (z, 2 r) \subseteq Ω$ , which covers $K^{'}$ because $Ω$ is open; compactness of $K^{'}$ yields finitely many balls $B (z_{l}, r_{l})$ , $l < m$ , with $K^{'} \subseteq ⋃_{l} B (z_{l}, r_{l})$ and $B (z_{l}, 2 r_{l}) \subseteq Ω$ , and $ϱ : = \min_{l} r_{l} > 0$ because $K^{'}$ is nonempty. Uniform continuity of $c$ on the compact interval $[0, 1]$ by [F7] at $ε = ϱ / 2$ gives $δ > 0$ such that $∣ s - s^{'} ∣ < δ$ implies $∣ c (s) - c (s^{'}) ∣_{2} < ϱ / 2$ . Choose $m \geq 1$ with $1 / m < δ$ by [F8] and set $s_{j} : = j / m$ . For each $j < m$ the point $c (s_{j})$ lies in some $B (z_{l}, r_{l})$ , and $∣ c (s_{j + 1}) - z_{l} ∣_{2} \leq ∣ c (s_{j + 1}) - c (s_{j}) ∣_{2} + ∣ c (s_{j}) - z_{l} ∣_{2} < ϱ / 2 + r_{l} \leq \frac{3}{2} r_{l} < 2 r_{l}$ , so both $c (s_{j})$ and $c (s_{j + 1})$ lie in the convex ball $B (z_{l}, 2 r_{l}) \subseteq Ω$ and the segment joining them is contained in $Ω$ ; concatenating these finitely many segments gives a piecewise- $C^{1}$ path in $Ω$ from $p$ to $q$ .

3.1F3F7F8step 1.1step 2.2

Mesh for a closed loop: let $γ : [0, 1] \to Ω$ be a closed piecewise- $C^{1}$ path with $p : = γ (0) = γ (1)$ . Regarded as a based loop at $p$ , it is path-homotopic relative to the endpoints to the constant loop at $p$ (Simply connected topological spaces and [F2]), so there is a continuous $H : [0, 1]^{2} \to Ω$ with $H (s, 0) = γ (s)$ , $H (s, 1) = p$ and $H (0, t) = H (1, t) = p$ by [F3]. The image $K : = H ([0, 1]^{2})$ is compact by [F7], and as in step 2.2 compactness of $K$ together with openness of $Ω$ yields finitely many balls $B (z_{l}, r_{l})$ with $K \subseteq ⋃_{l} B (z_{l}, r_{l})$ , $B (z_{l}, 2 r_{l}) \subseteq Ω$ and $ϱ : = \min_{l} r_{l} > 0$ . Uniform continuity of $H$ on the compact square at $ε = ϱ / 2$ gives $δ > 0$ such that $∣ u - u^{'} ∣_{2} < δ$ implies $∣ H (u) - H (u^{'}) ∣_{2} < ϱ / 2$ ; choose $m \geq 1$ with $2 / m < δ$ , possible by [F8], and consider the grid cells $C_{j, k} : = [j / m, (j + 1) / m] \times [k / m, (k + 1) / m]$ , $j, k < m$ . Any two points $u, u^{'}$ of a cell differ in each coordinate by at most $1 / m$ , so $∣ u - u^{'} ∣_{2} \leq 2 / m < δ$ and therefore $∣ H (u) - H (u^{'}) ∣_{2} < ϱ / 2$ ; writing $u_{j, k} : = (j / m, k / m)$ for the lower-left corner of $C_{j, k}$ we have $H (u_{j, k}) \in K \subseteq ⋃_{l} B (z_{l}, r_{l})$ , so $H (u_{j, k}) \in B (z_{l}, r_{l})$ for some $l$ .

4.1F5step 2.1step 3.1

Cell containment, cell loops and cancellation: for a cell $C_{j, k}$ with $H (u_{j, k}) \in B (z_{l}, r_{l})$ as in step 3.1, every $z \in C_{j, k}$ satisfies $∣ H (z) - z_{l} ∣_{2} \leq ∣ H (z) - H (u_{j, k}) ∣_{2} + ∣ H (u_{j, k}) - z_{l} ∣_{2} < ϱ / 2 + r_{l} \leq \frac{3}{2} r_{l} < 2 r_{l}$ , so $H (C_{j, k}) \subseteq B (z_{l}, 2 r_{l})$ ; the four corner images of $C_{j, k}$ therefore lie in this ball, and the piecewise-linear closed loop $λ_{j, k}$ running through them in the order lower-left, lower-right, upper-right, upper-left has its trace in the convex ball $B (z_{l}, 2 r_{l})$ , so $\int_{λ_{j, k}} A \cdot d r = 0$ by step 2.1. Summing over all $m^{2}$ cells via the additivity and reversal formulas of [F5]: every interior edge of the grid is traversed by the two cells sharing it in opposite directions, so those contributions cancel, while the right, top and left boundary edges are constant segments at the point $p$ , because $H (0, t) = H (1, t) = H (s, 1) = p$ by step 3.1, and constant paths have zero integral; hence $0 = \sum_{j, k < m} \int_{λ_{j, k}} A \cdot d r = \sum_{j < m} \int_{σ_{j}} A \cdot d r$ , where $σ_{j}$ is the straight segment from $H (u_{j, 0}) = γ (j / m)$ to $H (u_{j + 1, 0}) = γ ((j + 1) / m)$ .

5.1F4step 2.1step 4.1

Comparison of the loop with its chords: the restricted arcs $γ_{j} : = γ ∣_{[j / m, (j + 1) / m]}$ are piecewise- $C^{1}$ and satisfy $\int_{γ} A \cdot d r = \sum_{j < m} \int_{γ_{j}} A \cdot d r$ by [F4]; the trace of $γ_{j}$ is the bottom edge of the cell $C_{j, 0}$ under $H$ , hence is contained in $B (z_{l (j)}, 2 r_{l (j)})$ for the ball assigned to that cell in step 4.1, and the chord $σ_{j}$ joins the same two endpoints $γ (j / m)$ and $γ ((j + 1) / m)$ inside the same convex ball. By step 2.1 the integral of $A$ over a piecewise- $C^{1}$ arc in that ball depends only on its endpoints, so $\int_{γ_{j}} A \cdot d r = \int_{σ_{j}} A \cdot d r$ for every $j$ , and step 4.1 gives $\int_{γ} A \cdot d r = \sum_{j < m} \int_{γ_{j}} A \cdot d r = \sum_{j < m} \int_{σ_{j}} A \cdot d r = 0$ .

6.1F2F5step 5.1

Loop vanishing on $Ω$ : a path on a singleton interval has integral zero by definition; otherwise let $γ : [a, b] \to Ω$ be any closed piecewise- $C^{1}$ path. The affine reparametrization $h (t) : = a + (b - a) t$ of $[0, 1]$ onto $[a, b]$ is an oriented piecewise- $C^{1}$ reparametrization with increasing derivative, so by [F5] it suffices to prove $\int_{γ \circ h} A \cdot d r = 0$ , and $γ \circ h$ is a closed piecewise- $C^{1}$ path on $[0, 1]$ ; step 5.1 (applied to $γ \circ h$ , which by [F2] is path-homotopic relative to the endpoints to the constant loop at its basepoint, the existence of the homotopy $H$ being the sole hypothesis used there beyond steps 3.1 and 4.1) therefore gives $\int_{γ} A \cdot d r = 0$ . Hence the integral of $A$ vanishes along every closed piecewise- $C^{1}$ path in $Ω$ .

7.1F5step 6.1

Path independence on $Ω$ : let $γ_{0}, γ_{1} : [0, 1] \to Ω$ be piecewise- $C^{1}$ with the same initial point and the same terminal point. Then the concatenation $γ_{0} * γ_{1}^{-}$ is a closed piecewise- $C^{1}$ path in $Ω$ , and by [F5] $\int_{γ_{0} * γ_{1}^{-}} A \cdot d r = \int_{γ_{0}} A \cdot d r - \int_{γ_{1}} A \cdot d r$ ; step 6.1 makes the left-hand side zero, so $\int_{γ_{0}} A \cdot d r = \int_{γ_{1}} A \cdot d r$ . For paths on general intervals $[a, b]$ and $[c, d]$ the same conclusion follows after composing with the increasing affine reparametrizations onto $[0, 1]$ , which leave the integrals unchanged by [F5]; hence the $A$ -integral is path-independent on $Ω$ .

8.1step 2.2step 7.1

Definition of the primitive: fix a basepoint $p_{0} \in Ω$ , which exists because $Ω$ is nonempty, and let $y \in Ω$ . By step 2.2 there exists at least one piecewise- $C^{1}$ path in $Ω$ from $p_{0}$ to $y$ , and by step 7.1 the value of $\int A \cdot d r$ is the same for all such paths; so the relation consisting of the pairs $(y, \int_{η} A \cdot d r)$ for piecewise- $C^{1}$ paths $η$ from $p_{0}$ to $y$ is a single-valued relation on $Ω$ , and it defines a function $\tilde{F} : Ω \to R$ by $\tilde{F} (y) : = \int_{p_{0}}^{y} A \cdot d r$ , the common value of that integral. No selection of paths is needed for this definition: at each $y$ there is a path and the value is unique, so $\tilde{F}$ is a well-defined function without any choice principle.

9.1F5step 2.1step 8.1

The primitive is $C^{2}$ with $\nabla \tilde{F} = A$ : let $z \in Ω$ and let $B = B (z, ϱ) \subseteq Ω$ be an open ball, which exists because $Ω$ is open; for $y \in B$ the straight segment $η$ from $z$ to $y$ lies in the convex ball $B$ . Fix a piecewise- $C^{1}$ path $γ_{z}$ in $Ω$ from $p_{0}$ to $z$ ; then $γ_{z} * η$ is a piecewise- $C^{1}$ path from $p_{0}$ to $y$ , so by the definition of $\tilde{F}$ in step 8.1 and the additivity formula of [F5] we get $\tilde{F} (y) = \int_{γ_{z} * η} A \cdot d r = \tilde{F} (z) + \int_{η} A \cdot d r$ , and step 2.1 on the ball $B$ gives $\int_{η} A \cdot d r = φ_{B} (y) - φ_{B} (z)$ for the $C^{2}$ local primitive $φ_{B}$ of step 2.1. Hence $\tilde{F} (y) = φ_{B} (y) + c_{B}$ on $B$ with the constant $c_{B} : = \tilde{F} (z) - φ_{B} (z)$ ; consequently $\tilde{F}$ is $C^{2}$ on $B$ and $\partial_{i} \tilde{F} = \partial_{i} φ_{B} = a_{i}$ on $B$ for every $i$ . Since $z \in Ω$ was arbitrary, $\tilde{F}$ has continuous first and second partial derivatives on all of $Ω$ and $\nabla \tilde{F} = A$ there.

10.1step 1.1step 6.1step 7.1step 9.1∎

Assembling the conclusions: if the coefficients $a_{i}$ , hence the field $A$ , are smooth, then $\partial_{i} \tilde{F} = a_{i}$ is smooth for every $i$ by step 9.1, so all higher partial derivatives of $\tilde{F}$ exist and are continuous and $\tilde{F}$ is smooth ( $C^{k}$ maps and multi-index derivative notation in Euclidean space). Now transport back to $U$ : define $F : = \tilde{F} \circ x$ ; since $x$ is a diffeomorphism by [F1] and $\tilde{F}$ is $C^{2}$ (smooth when $A$ is smooth), also $F$ is $C^{2}$ (respectively smooth), and in the chart $x$ the coefficients of $d F$ are the partial derivatives $\partial_{i} \tilde{F} = a_{i}$ , so that $d F = α$ on $U$ by the conventions of the Statement. Moreover, if $γ_{0}, γ_{1}$ are piecewise- $C^{1}$ paths in $U$ with the same endpoints, then $x \circ γ_{0}$ and $x \circ γ_{1}$ are piecewise- $C^{1}$ paths in $Ω$ with the same endpoints and, by the definition of the integral in the conventions, $\int_{γ_{0}} α = \int_{x \circ γ_{0}} A \cdot d r = \int_{x \circ γ_{1}} A \cdot d r = \int_{γ_{1}} α$ by step 7.1; and if $γ$ is a piecewise- $C^{1}$ loop in $U$ then $x \circ γ$ is a closed piecewise- $C^{1}$ path in $Ω$ and $\int_{γ} α = \int_{x \circ γ} A \cdot d r = 0$ by step 6.1. This proves (a) and (b), and the extra smoothness assertion when $α$ is smooth.

Remarks

What is used and what is not. The classical proof of the converse direction — a closed 1-form on a simply connected open set is exact — is reduced here to three published inputs on the coefficient side: the radial (star-shaped) local primitive, the homotopy-invariant mesh argument of steps 3.1–5.1, and the telescoping property on balls of step 2.1. The mesh argument uses only Heine–Borel, Heine–Cantor uniform continuity and the Archimedean reciprocal; in particular it does not invoke de Rham theory, smooth approximation, or the Poincaré lemma for more general domains, and it uses no choice principle: the finitely many ball and grid choices are finite, the homotopy is a single object, and the primitive is defined by uniqueness of the path integral rather than by a selection of paths.
The global C1-to-C2 statement. The retrieved sources on the line-integral side supply the smooth global result and the local star-shaped C1-to-C2 result; the global C1 conclusion above is obtained by the finite grid argument of steps 3.1–5.1, which is written out here and is not claimed to be a verbatim quotation of either source. This is the exact source adaptation recorded for the scaffolding of this item, and it is the honest division of labour between the cited texts and the local argument.

A closed 1-form on a simply connected open subset of the affine model has a primitive

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources