TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pendingjudge 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.

Gauss-Codazzi and Maxwell initial constraints

Statement

Let $(g, F)$ be a smooth source-free electrovacuum solution of Electrovacuum tensor Cauchy system on a neighborhood of a smooth spacelike embedded hypersurface $i : Σ ↪ M$ . Let $n$ be its future unit normal, $h = i^{*} g$ , $K (X, Y) = g (\nabla_{X} n, Y)$ , and let $(e, b)$ be its observer electric/magnetic data. Then the induced tuple $(Σ, h, K, e, b)$ satisfies all four constraints in Constrained electrovacuum initial data, namely the two Maxwell divergence constraints and

$R (h) + ({tr}_{h} K)^{2} - ∣ K ∣_{h}^{2} = 2 Λ + \frac{κ}{μ_{0}} (∣ e ∣_{h}^{2} + ∣ b ∣_{h}^{2}),$

$D^{j} K_{j i} - D_{i} {tr}_{h} K = - \frac{κ}{μ_{0}} (e \times_{h} b)_{i} .$

This is a necessary-constraint theorem for an existing smooth solution. It is not a sufficiency or local-existence theorem for arbitrary data satisfying these equations.

Facts & Assumptions

Given: A smooth oriented, time-oriented Lorentzian four-manifold, a smooth source-free solution $(g, F)$ , and a smooth spacelike hypersurface with the induced data above.

[A1]

Electrovacuum tensor Cauchy system: $G + Λ g = κ T^{E M}$ , $d F = 0$ , and $d (⋆_{g} F) = 0$ .

[F1]

Constrained electrovacuum initial data: $K = + \frac{1}{2} L_{n} h$ and the four displayed constraints are the definition of constrained data.

[F2]

Maxwell stress algebra and covariant conservation: $T^{E M} (n, n) = (∣ e ∣_{h}^{2} + ∣ b ∣_{h}^{2}) / (2 μ_{0})$ and $T^{E M} (n, V) = - h (e \times_{h} b, V) / μ_{0}$ .

[F3]

Gauss-Codazzi decomposition in Gaussian normal coordinates and the constraint equations in terms of the induced metric and second fundamental form: for this $K$ convention, $G (n, n) = \frac{1}{2} (R (h) + ({tr}_{h} K)^{2} - ∣ K ∣_{h}^{2})$ and $G (n, V) = D^{j} K_{j i} V^{i} - D_{V} {tr}_{h} K$ .

[F4]

Observer electric/magnetic reconstruction and invariants and Lorentzian exterior calculus and Hodge star: after locally extending the smooth normal to an observer field, the pointwise decomposition in a positively oriented normal tetrad is $F = - θ^{0} \land E + ⋆_{h} B$ and $⋆_{g} F = θ^{0} \land B + ⋆_{h} E$ , where $E = e^{♭}$ and $B = b^{♭}$ are the spatial covectors of Constrained electrovacuum initial data. Pulling back to the slice removes the terms containing $θ^{0}$ .

[F5]

On the oriented Riemannian three-manifold $(Σ, h)$ , the Hodge star $⋆_{h} : Λ^{k} T^{*} Σ \to Λ^{3 - k} T^{*} Σ$ is the unique bundle map satisfying $α \land ⋆_{h} β = ⟨ α, β ⟩_{h} {vol}_{h}$ . In a positively oriented orthonormal coframe $(e^{1}, e^{2}, e^{3})$ , $⋆_{h} e^{1} = e^{2} \land e^{3}$ , $⋆_{h} e^{2} = e^{3} \land e^{1}$ , and $⋆_{h} e^{3} = e^{1} \land e^{2}$ ; by linearity this is $⋆_{h} v^{♭} = ι_{v} {vol}_{h}$ . In a positively oriented coordinate chart, ${vol}_{h} = \sqrt{\det h} d x^{1} \land d x^{2} \land d x^{3}$ .

[F6]

For the smooth embedding $i : Σ ↪ M$ , pullback commutes with exterior differentiation: $d_{Σ} i^{*} ω = i^{*} d_{M} ω$ for every smooth differential form $ω$ . In slice coordinates where $i (x^{1}, x^{2}, x^{3}) = (0, x^{1}, x^{2}, x^{3})$ , pullback deletes every term containing $d x^{0}$ ; differentiating the remaining coefficients in $x^{1}, x^{2}, x^{3}$ gives the same terms as pulling back $d_{M} ω$ , which proves the identity in these coordinates.

Proof

1.1A1F4F5F6algebra

Fix a point of $Σ$ and choose an oriented slice chart, which is possible by Embedded submanifolds and slice charts. A local smooth extension of $n$ along $Σ$ is supplied by The future unit normal, induced metric and second fundamental form of a spacelike hypersurface; after shrinking it remains future timelike and normalization makes it an observer field. In a positively oriented local orthonormal tetrad $(n, e_{1}, e_{2}, e_{3})$ , [F4] gives $i^{*} F = ⋆_{h} b^{♭}$ and $i^{*} (⋆_{g} F) = ⋆_{h} e^{♭}$ . By the coordinate pullback identity [F6], $d_{Σ} i^{*} F = i^{*} d_{M} F$ and $d_{Σ} i^{*} (⋆_{g} F) = i^{*} d_{M} (⋆_{g} F)$ , so [A1] yields $d_{Σ} (⋆_{h} b^{♭}) = 0$ and $d_{Σ} (⋆_{h} e^{♭}) = 0$ . To convert these into divergences, [F5] gives $⋆_{h} v^{♭} = ι_{v} {vol}_{h}$ . In oriented coordinates, $d_{Σ} (ι_{v} {vol}_{h}) = \partial_{i} (\sqrt{\det h} v^{i}) d x^{1} \land d x^{2} \land d x^{3}$ . The Levi-Civita formula gives $Γ^{i}_{i k} = \frac{1}{2} h^{i j} \partial_{k} h_{i j}$ ; differentiating the determinant yields $\partial_{k} \log \sqrt{\det h} = \frac{1}{2} h^{i j} \partial_{k} h_{i j}$ . Hence this exterior derivative equals $(D_{i} v^{i}) {vol}_{h}$ . Therefore $D_{i} b^{i} = 0$ and $D_{i} e^{i} = 0$ at the chosen point, and hence throughout $Σ$ .

1.2A1F2F3algebra

Apply [F3] to the existing solution in [A1]. The normal-normal projection of $G + Λ g = κ T^{E M}$ gives $\frac{1}{2} (R (h) + τ^{2} - ∣ K ∣^{2}) - Λ = κ T^{E M} (n, n)$ because $g (n, n) = - 1$ . Substitute [F2] and multiply by $2$ to obtain the Hamiltonian constraint.

1.3A1F2F3algebra

For any tangent $V$ , the normal-tangential projection gives $G (n, V) = κ T^{E M} (n, V)$ because $g (n, V) = 0$ . Substitute [F2]–[F3] to get $(D^{j} K_{j i} - D_{i} τ) V^{i} = - (κ / μ_{0}) h (e \times_{h} b, V)$ . Since this holds for every tangent $V$ , the two covectors are equal, proving the momentum constraint.

2.1F1step 1.1step 1.2step 1.3∎

The Maxwell divergence identities from 1.1 and the Einstein normal projections from 1.2–1.3 are exactly the four constraint equations in [F1]. If $Σ$ is nonempty, the induced tuple is constrained electrovacuum initial data in that definition; if $Σ$ is empty, the four equations hold vacuously.

Gauss-Codazzi and Maxwell initial constraints

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources