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

Local existence for the reduced Einstein equation from Cauchy data on a spacelike slice

Statement

Assume Countable Choice ${A C}_{ω}$ (The Axiom of Countable Choice ( ${A C}_{ω}$ )), carrying the hypotheses of the analytic suppliers used below.

Let $M$ be a smooth four-manifold carrying a chart $(x^{0} = t, x^{1}, x^{2}, x^{3})$ whose domain $U$ contains the slice $Σ : = {t = 0}$ , let $\overset{ˉ}{g}$ be a smooth background metric on $U$ with its Levi--Civita connection $\overset{ˉ}{\nabla}$ , and let $T$ be a smooth symmetric covariant $2$ -tensor on $U$ together with the background-covariant derivatives needed below (the matter field data). Suppose smooth functions $g_{a b}^{0}, g_{a b}^{1}$ on $Σ \cap U$ are given such that:

$g^{0}$ is a smooth field of Lorentzian bilinear forms on the restricted spacetime tangent bundle $T M ∣_{Σ \cap U}$ , whose restriction to $T Σ$ is positive definite. Write $g_{a b}^{0}$ for its components in the given spacetime chart; its inverse components satisfy $g_{0}^{00} < 0$ and the spatial block $(g_{0}^{i j})$ is positive definite;
$g_{a b}^{1}$ is symmetric and agrees on $Σ$ with the components of ${\overset{ˉ}{\nabla}}_{0} g_{a b}$ for some smooth extension $g$ of $g^{0}$ to $U$ ;
the harmonic-gauge condition $H^{a} = 0$ holds on $Σ \cap U$ for the pair $(g, \overset{ˉ}{g})$ (The harmonic gauge vector, the reduced Einstein equation and the Einstein residual).

Then there is an open neighborhood $V \subseteq U$ of $Σ \cap U$ and a smooth metric $g$ on $V$ with $g ∣_{Σ \cap U} = g^{0}$ and ${\overset{ˉ}{\nabla}}_{0} g_{a b} ∣_{Σ \cap U} = g_{a b}^{1}$ , solving the reduced Einstein equation with the given background $\overset{ˉ}{g}$ and matter tensor $T$ (The harmonic gauge vector, the reduced Einstein equation and the Einstein residual) on $V$ .

Facts & Assumptions

Given: Countable Choice and the chart and slice, the background metric $\overset{ˉ}{g}$ , the matter tensor $T$ , and data $g^{0}, g^{1}$ satisfying conditions 1--3.

[L1]

The reduced Einstein equation is equivalent, on a region where the metric is Lorentzian, $g^{00} < 0$ and $(g^{i j})$ is positive definite, to a first-order quasilinear system for $u = (g_{a b}, p_{a b} = {\overset{ˉ}{\nabla}}_{0} g_{a b}, q_{a b i} = {\overset{ˉ}{\nabla}}_{i} g_{a b})$ whose coefficient of the time derivative is the positive definite block matrix $diag (I, - g^{00} I, g^{i j} I)$ and whose spatial coefficients are symmetric (Principal part of the reduced Einstein operator and its first-order symmetric hyperbolic reduction clause (b)).

[L2]

Local well-posedness and finite-speed independence for symmetric hyperbolic systems: solutions exist on a neighborhood of the initial slice and are independent, on the domain of dependence, of the way the data and coefficients are extended beyond a coordinate patch (Local well-posedness and finite-speed independence of the extension for symmetric hyperbolic systems on a coordinate neighbourhood, Local existence of Sobolev and classical solutions of a periodic symmetric hyperbolic system, uniform on bounded H^s data); smooth data give smooth solutions (Smooth data give smooth solutions of a periodic symmetric hyperbolic system on the existence interval).

[L3]

The data are smooth on the slice, and the metric properties $g_{0}^{00} < 0$ and positive definite spatial block persist in a neighborhood of the slice by continuity; a smooth extension of the data to $U$ exists ( $C^{r}$ and smooth maps between smooth manifolds, Smooth covariant 2-tensor fields on a smooth manifold).

Proof

technique · direct

1.1L1L3algebra

(Reduction to a first-order symmetric hyperbolic initial value problem.) Extend $g^{0}, g^{1}$ to smooth fields on $U$ with $g_{a b}^{1} = {\overset{ˉ}{\nabla}}_{0} g_{a b}$ at $t = 0$ [L3], and set $p_{a b} : = g_{a b}^{1}$ , $q_{a b i} : = {\overset{ˉ}{\nabla}}_{i} g_{a b}^{0}$ initially. By [L1] the reduced equation, together with the definition of $(p, q)$ , is the first-order quasilinear system $S (u) = 0$ on $U$ ; at $t = 0$ the time matrix of $S$ is positive definite because $g_{0}^{00} < 0$ and $(g_{0}^{i j}) > 0$ , and positivity persists in an open neighborhood of the slice by [L3].

2.1step 1.1L2algebra

(Local solution and independence.) Choose a coordinate ball $B ⋐ U$ meeting $Σ \cap U$ and cut off the data and the coefficient functions outside $B$ ; the resulting system is a periodic symmetric hyperbolic system after identifying a neighborhood of $B$ with an open subset of $T_{2 π}^{3}$ and extending by constants. By [L2] it has a smooth solution on a time interval around $0$ ; by the finite-speed independence clause of [L2], restricted to the domain of dependence of $Σ \cap B$ the solution depends only on the data and coefficients inside the patch, so the local solutions on overlapping balls agree and patch to a solution of $S (u) = 0$ on a neighborhood $V$ of $Σ \cap U$ .

3.1step 2.1L1algebra∎

(Return to the second-order equation.) The metric equation gives ${\overset{ˉ}{\nabla}}_{0} g = p$ . Define the spatial derivative residual $Z_{a b i} : = q_{a b i} - {\overset{ˉ}{\nabla}}_{i} g_{a b}$ , initially zero. The transport equation for $q$ contains precisely the commutator $C_{a b i} = - {\overset{ˉ}{R}}^{c}_{a 0 i} g_{c b} - {\overset{ˉ}{R}}^{c}_{b 0 i} g_{a c}$ . Subtracting the background derivative identity for ${\overset{ˉ}{\nabla}}_{i} g$ cancels that term and gives a homogeneous linear ODE along each coordinate time line for $Z$ (in component form $\partial_{t} Z_{a b i} = {\overset{ˉ}{Γ}}^{c}_{0 a} Z_{c b i} + {\overset{ˉ}{Γ}}^{c}_{0 b} Z_{a c i}$ ; the derivative-slot connection terms cancel by background torsion-freeness). Its zero initial value forces $Z = 0$ , as follows by differentiating its Euclidean squared norm, bounding its derivative by a continuous multiple of itself on each compact time segment, and multiplying by the corresponding exponential integrating factor. Thus $p = {\overset{ˉ}{\nabla}}_{0} g$ and $q_{i} = {\overset{ˉ}{\nabla}}_{i} g$ throughout the local time collars. Substitution in the metric wave equation recovers the exact reduced Einstein equation with the stated data. This gives the asserted smooth solution.

Remarks

Role. This is E1's existence theorem for the gauge-reduced equation; E2 supplies the geometric data $g^{0}, g^{1}$ from $(h, K)$ and removes the background dependence by geometric uniqueness, and E3 verifies the matter reductions.

Local existence for the reduced Einstein equation from Cauchy data on a spacelike slice

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources