LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generated

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.

Radial primitives for closed one- and two-forms

Statement

Let $D \subseteq R^{4}$ be an open set star-shaped about $p \in D$ , meaning $p + t (x - p) \in D$ for every $x \in D$ and $0 \leq t \leq 1$ . Let $F = \frac{1}{2} F_{a b} d x^{a} \land d x^{b}$ be a smooth real closed two-form on $D$ . Use Einstein summation over coordinate indices $a, b, c \in {0, 1, 2, 3}$ . Define

A_{b} (x) : = \int_{0}^{1} t (x - p)^{a} F_{a b} (p + t (x - p)) d t .

Then $A = A_{b} d x^{b}$ is a smooth real one-form on $D$ and $d A = F$ . More generally, if $α = α_{a} d x^{a}$ is a smooth closed one-form on $D$ , then

χ (x) : = \int_{0}^{1} (x - p)^{a} α_{a} (p + t (x - p)) d t

is smooth and $d χ = α$ . The first formula gives a local potential for every smooth closed two-form in a star-shaped coordinate chart; it does not assert global exactness.

Facts & Assumptions

Given: A star-shaped open coordinate domain $D \subseteq R^{4}$ , its center $p$ , and the smooth closed forms $F$ and, for the final assertion, $α$ .

[F1]

Oriented Lorentzian fields, observers and coordinate conventions: a smooth real $k$ -form is a smooth section of $⋀^{k} T^{*} M$ ; in a coordinate chart its coefficients are smooth functions.

[F2]

Lorentzian exterior calculus and Hodge star: $d$ has the alternating coordinate formula, and $d^{2} = 0$ . In particular $d F = 0$ means $\partial_{c} F_{a b} + \partial_{a} F_{b c} + \partial_{b} F_{c a} = 0$ , while $(d A)_{c b} = \partial_{c} A_{b} - \partial_{b} A_{c}$ .

[F3]

Leibniz's rule on a compact rectangle: an interior parameter derivative with a continuous extension may be passed through a Riemann integral: if an integrand and its parameter derivative are continuous on a compact rectangle, the parameter derivative passes through its Riemann integral.

[F4]

Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative: for a continuous function on a closed interval with a continuous integrable extension of its interior derivative, the integral of that derivative is the endpoint difference.

[F5]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: every continuous real function on a closed bounded interval is Riemann integrable.

[A1]

The typed finite-real, metric, power, sequence-limit and boundaryless conventions in the declared dependencies are authored earlier on this page. Their exact scopes remain separate: the sequence criterion assumes ${A C}_{ω}$ only for its reverse implication. The radial coefficient calculation below uses no selection from a countable family.

Proof

1.1givenF1F3algebra

Put $y = x - p$ . Fix $x_{0} \in D$ and choose a closed coordinate box $K \subset D$ with $x_{0}$ in its interior. The image of $K \times [0, 1]$ under $(x, t) \mapsto p + t (x - p)$ is compact and lies in $D$ , so the integrand $G_{b} (x, t) = t (x - p)^{a} F_{a b} (p + t (x - p))$ and every $x$ -partial derivative are continuous on $K \times [0, 1]$ . Fixing all but one coordinate, [F3] passes that parameter derivative through the integral on the corresponding compact rectangle; applying it repeatedly to each derivative shows that every partial derivative of $A_{b}$ exists and is continuous near $x_{0}$ . Since $x_{0}$ was arbitrary, $A_{b}$ is smooth on $D$ , and $A = A_{b} d x^{b}$ is a smooth one-form.

2.1givenF2F3step 1.1algebra

By the differentiation-under-the-integral justification in step 1.1, differentiate the integral and use antisymmetry to obtain $\partial_{c} A_{b} - \partial_{b} A_{c} = \int_{0}^{1} (2 t F_{c b} (p + t y) + t^{2} y^{a} (\partial_{c} F_{a b} - \partial_{b} F_{a c}) (p + t y)) d t$ . The closure identity in [F2] gives $\partial_{c} F_{a b} - \partial_{b} F_{a c} = \partial_{a} F_{c b}$ . Thus the integrand is $\frac{d}{d t} (t^{2} F_{c b} (p + t y))$ .

3.1givenF2F4F5step 2.1algebra

The function $t \mapsto t^{2} F_{c b} (p + t y)$ is continuous on $[0, 1]$ , differentiable on $(0, 1)$ , and its derivative extends continuously to both endpoints, hence is integrable by [F5]. The Newton–Leibniz formula [F4] evaluates the integral as $F_{c b} (x) - 0$ , since $t^{2} F_{c b} (p + t y) = 0$ at $t = 0$ . Therefore every coefficient of $d A$ equals the corresponding coefficient of $F$ , so $d A = F$ .

4.1givenF2F3F4F5step 1.1algebra∎

For the one-form formula, [F3] applies to the smooth integrand on the same compact-image rectangles as in step 1.1, so $χ$ is smooth. Closedness gives $\partial_{b} α_{a} = \partial_{a} α_{b}$ , and hence $\partial_{b} χ = \int_{0}^{1} (α_{b} (p + t y) + t y^{a} \partial_{a} α_{b} (p + t y)) d t = \int_{0}^{1} \frac{d}{d t} (t α_{b} (p + t y)) d t = α_{b} (x)$ by [F4] and [F5]; the lower endpoint vanishes. Thus $d χ = α$ , proving this local gauge-difference assertion without assuming a global real phase.

Remarks

The radial calculation uses only the stated smoothness and star-shaped-domain hypotheses and the local exterior-derivative formula. The additional typed dependencies preserve the approved foundational conventions; their statements do not introduce a choice step into this explicit finite-interval calculation.

Depends on

Dependency tree · 2 levels

Sources

Victor Guillemin and Peter Haine, Differential Forms, MIT 18.952 text (2019), sections 2.4 and 2.6