LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge 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.

Sourced Maxwell sign and current conservation

Statement

Let $(M, g, N, o)$ be the smooth, boundaryless, oriented and time-oriented Lorentzian four-manifold of Oriented Lorentzian fields, observers and coordinate conventions, with signature $(-, +, +, +)$ , metric-selected connection $\nabla$ and oriented metric volume form ${v o l}_{g}$ . Let $F \in Ω^{2} (M)$ be a smooth real two-form and $j \in Γ (T M)$ a smooth vector field. Fix constants $μ_{0} > 0$ and $c > 0$ ; $μ_{0}$ is a real coefficient here, and $c$ is the positive coordinate conversion in $x^{0} = c t$ of Oriented Lorentzian fields, observers and coordinate conventions. Assume the mathematical field equations

$d F = 0, \nabla_{a} F^{a b} = - μ_{0} j^{b} .$

The equations are conditional hypotheses, not physical postulates in this mathematical item. Define $v \in Γ (T M)$ by $v^{b} : = \nabla_{a} F^{a b}$ and define the current three-form by $ι_{j} {v o l}_{g}$ , the contraction specified in The metric volume form, current flux through 3-faces and finite-chain charges. Then:

(a) Sign identity. On $M$ ,

$d (⋆_{g} F) = - ι_{v} {v o l}_{g} .$

Consequently the sourced equation is equivalently

$\nabla_{a} F^{a b} = - μ_{0} j^{b} ⟺ d (⋆_{g} F) = μ_{0} ι_{j} {v o l}_{g} .$

(b) Current conservation. Either equivalent sourced equation implies $\nabla_{a} j^{a} = 0$ . This conclusion requires the sourced equation and $μ_{0} > 0$ ; it does not require $d F = 0$ .

(c) Local component check. At any $p \in M$ , choose a positively oriented point-normal chart supplied by Point-normal and exponential coordinate charts of the metric-selected connection. In that chart, write $E_{i} (x) : = - c F_{0 i} (x)$ and $B_{i} (x) : = \frac{1}{2} ϵ_{i j k} F_{j k} (x)$ , where $ϵ_{123} = + 1$ and $ϵ_{i j k}$ is alternating. These are local component abbreviations in the chosen chart, not global observer fields. With $div E : = \partial_{i} E_{i}$ , $(curl E)_{k} : = ϵ_{k i j} \partial_{i} E_{j}$ , and similarly for $B$ , the pointwise component identities are

$v^{0} = - \frac{1}{c} div E, v^{k} = \frac{1}{c^{2}} \partial_{t} E_{k} - (curl B)_{k},$

$(d ⋆_{g} F)_{123} = \frac{1}{c} div E, (d ⋆_{g} F)_{0 i j} = ϵ_{i j k} (\frac{1}{c^{2}} \partial_{t} E_{k} - (curl B)_{k}),$

$(d F)_{123} = div B, (d F)_{0 i j} = \frac{ϵ_{i j k}}{c} (\partial_{t} B_{k} + (curl E)_{k}),$

where $\partial_{t} : = c \partial_{0}$ . The equations are pointwise identities in normal coordinates; they do not assert that these component abbreviations form global three-vector fields on curved spacetime.

On an open flat Minkowski domain with a fixed inertial Cartesian chart $x^{0} = c t$ , define $ρ : = j^{0} / c$ , $J^{i} : = j^{i}$ , and $ϵ_{0} : = (μ_{0} c^{2})^{- 1}$ . The same component formulas at every point give

$div E = \frac{ρ}{ϵ_{0}}, curl B - \frac{1}{c^{2}} \partial_{t} E = μ_{0} J, div B = 0, \partial_{t} B + curl E = 0.$

These are a coordinate reduction of the stated tensor and form equations, not claims that the smooth fields describe an experiment.

Facts & Assumptions

Given: The geometric data, fields and positive coefficients specified in the Statement.

[F1]

Oriented Lorentzian fields, observers and coordinate conventions defines a smooth, boundaryless, oriented, time-oriented Lorentzian four-manifold of signature $(-, +, +, +)$ , its independent orientation and metric volume form, its torsion-free metric-selected connection, and the positive scale $c$ in $x^{0} = c t$ .

[F2]

Lorentzian exterior calculus and Hodge star defines $⋆_{g}$ by the Lorentzian metric and orientation. In an oriented orthonormal coframe its two-form components are $(⋆_{g} F)_{a b} = \frac{1}{2} ({v o l}_{g})_{a b c d} F^{c d}$ , and $d^{2} = 0$ .

[F3]

Existence of a smooth future-directed tetrad field near every event supplies a smooth future-directed orthonormal tetrad near each point, but does not impose its orientation relative to $o$ . At $p$ , reversing one of its three spacelike legs when necessary makes the ordered basis positively oriented while preserving orthonormality and the future direction of its timelike leg. The geodesic initial-value problem and the exponential map of the metric-selected connection and Point-normal and exponential coordinate charts of the metric-selected connection apply to any such orthonormal basis and supply a point-normal exponential chart whose coordinate orientation is positive and which satisfies $g_{a b} (p) = η_{a b}$ , $Γ^{a}_{b c} (p) = 0$ , and $\partial_{a} g_{b c} (p) = 0$ . This is a pointwise normal-coordinate statement; it asserts no flat neighborhood.

[F4]

The metric volume form, current flux through 3-faces and finite-chain charges defines the current three-form as $ι_{j} {v o l}_{g}$ . For smooth $j$ , Divergence, Stokes flux balance and the non-null face formula for a Lorentzian current proves $d (ι_{j} {v o l}_{g}) = (\nabla_{a} j^{a}) {v o l}_{g}$ .

[F5]

The ambient tangent-bundle conventions inherited through the geometric suppliers use ${A C}_{ω}$ , the axiom that every countable family of nonempty sets has a choice function (The Axiom of Countable Choice ( ${A C}_{ω}$ )). The finite component calculations below add no arbitrary-choice assumption.

[A1]

Fix constants $μ_{0} > 0$ and $c > 0$ . The equations $d F = 0$ and $\nabla_{a} F^{a b} = - μ_{0} j^{b}$ are hypotheses of the conditional mathematical result; no physical postulate or measured value of either coefficient is assumed.

[A2]

For the final flat-coordinate specialization only, assume an open domain with Minkowski metric $η = diag (- 1, 1, 1, 1)$ in an inertial Cartesian chart $x^{0} = c t$ , and define $ρ = j^{0} / c$ , $J^{i} = j^{i}$ and $ϵ_{0} = (μ_{0} c^{2})^{- 1}$ .

Proof

Given: The hypotheses of the Statement and labelled items [F1]–[F5], [A1], and [A2] when the flat specialization is used.

1.1givenF1F2F3F5algebraconstruct

Fix $p \in M$ . By the local tetrad theorem in [F3], choose a future-directed orthonormal tetrad at $p$ ; if necessary reverse one spatial leg to make the basis positively oriented relative to $o$ . This leaves its orthonormality and future-directed timelike leg unchanged. Apply the point-normal exponential-chart theorem of [F3] to this basis. In this chart the inverse metric and volume coefficients have zero first derivatives at $p$ : differentiating $g^{a c} g_{c b} = δ^{a}_{b}$ shows $\partial g^{a b} (p) = 0$ , and differentiating $w = \sqrt{∣ \det (g_{a b}) ∣}$ gives $\partial w (p) = 0$ when $\partial g_{a b} (p) = 0$ . Thus the first derivatives of the coefficient map in the Hodge formula [F2] vanish at $p$ . Define the local component functions $E_{i} = - c F_{0 i}$ and $B_{i} = \frac{1}{2} ϵ_{i j k} F_{j k}$ . Raising indices with $η$ and using [F2] gives $F^{0 i} = E_{i} / c$ , $F^{i 0} = - E_{i} / c$ , $F^{i j} = ϵ_{i j k} B_{k}$ , $(⋆_{g} F)_{0 i} = B_{i}$ , and $(⋆_{g} F)_{i j} = ϵ_{i j k} E_{k} / c$ at $p$ .

2.1givenF1F2F3F4step 1.1algebra

Since $Γ (p) = 0$ , the divergence components at $p$ are $v^{0} = \partial_{i} F^{i 0} = - div E / c$ and $v^{k} = \partial_{0} F^{0 k} + \partial_{i} F^{i k} = c^{- 2} \partial_{t} E_{k} - (curl B)_{k}$ . The coordinate formula for $d$ and the vanishing first derivatives of the Hodge coefficients in step 1.1 give $(d ⋆_{g} F)_{123} = \partial_{i} E_{i} / c$ and $(d ⋆_{g} F)_{0 i j} = ϵ_{i j k} (c^{- 2} \partial_{t} E_{k} - (curl B)_{k})$ . In the same oriented chart, $(ι_{v} {v o l}_{g})_{123} = v^{0}$ and $(ι_{v} {v o l}_{g})_{0 i j} = - ϵ_{i j k} v^{k}$ . These four independent components prove $d (⋆_{g} F) = - ι_{v} {v o l}_{g}$ at $p$ . Since $p$ was arbitrary and both sides are smooth three-forms, the identity holds on $M$ .

2.2givenF1F2step 1.1algebra

Because $\nabla$ is torsion-free by [F1], its symmetric connection coefficients cancel under total antisymmetrization, so $(d F)_{a b c} = 3 \partial_{[a} F_{b c]} = 3 \nabla_{[a} F_{b c]}$ . In the normal chart of step 1.1, substitution of $F_{0 i} = - E_{i} / c$ and $F_{i j} = ϵ_{i j k} B_{k}$ gives $(d F)_{123} = div B$ and $(d F)_{0 i j} = ϵ_{i j k} (\partial_{t} B_{k} + (curl E)_{k}) / c$ . These are pointwise component identities for the local chart functions; they do not make $E_{i}, B_{i}$ global fields on $M$ .

3.1givenA1F1F2F4step 2.1algebra

Substituting $v^{b} = \nabla_{a} F^{a b} = - μ_{0} j^{b}$ into step 2.1 yields $d (⋆_{g} F) = - ι_{- μ_{0} j} {v o l}_{g} = μ_{0} ι_{j} {v o l}_{g}$ . Conversely, if this form equation holds, step 2.1 gives $ι_{v + μ_{0} j} {v o l}_{g} = 0$ . At each point contraction with a nonvanishing four-form is an isomorphism from the four-dimensional tangent space to the space of three-covectors, so $v + μ_{0} j = 0$ . This proves the equivalence in the Statement.

4.1givenA1F2F4step 3.1algebra

Apply $d$ to the form equation in step 3.1. By [F2], $d^{2} (⋆_{g} F) = 0$ ; since $μ_{0}$ is a nonzero constant, $d (ι_{j} {v o l}_{g}) = 0$ . The exact identity in [F4] then gives $(\nabla_{a} j^{a}) {v o l}_{g} = 0$ . The volume form is nowhere zero, hence $\nabla_{a} j^{a} = 0$ throughout $M$ . This uses the sourced equation only and does not invoke $d F = 0$ .

5.1givenA2step 2.1step 2.2algebra∎

Under the additional flat-chart hypothesis [A2], the normal-coordinate component identities hold at every point in the same Cartesian chart. The time component of $v = - μ_{0} j$ is $- div E / c = - μ_{0} c ρ$ , giving $div E = ρ / ϵ_{0}$ . Its spatial components are $c^{- 2} \partial_{t} E - curl B = - μ_{0} J$ , or $curl B - c^{- 2} \partial_{t} E = μ_{0} J$ . The two formulas from step 2.2 give $div B = 0$ and $\partial_{t} B + curl E = 0$ . This is the stated flat-coordinate reduction.

Remarks

The sign is tied to the displayed convention $F_{0 i} = - E_{i} / c$ , orientation ${v o l}_{g} (e_{0}, e_{1}, e_{2}, e_{3}) = + 1$ , signature $(-, +, +, +)$ , and index order $\nabla_{a} F^{a b}$ . Carroll's full lecture notes use Gaussian units and write $\partial_{μ} F^{ν μ} = + 4 π J^{ν}$ ; antisymmetry rewrites this as $\partial_{μ} F^{μ ν} = - 4 π J^{ν}$ before translating coefficients. No field equation, current-conservation law, or global inertial chart is imported from a differently signed convention.

Sourced Maxwell sign and current conservation

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources