ExampleConstruction: AI-adaptedVerification: AI-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.

The maximal development of the flat vacuum data is Minkowski spacetime

Example

Assume Countable Choice and Dependent Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain) for the invoked general causal and maximal-development suppliers.

Take $Σ : = R^{3}$ , $h$ the Euclidean metric $δ$ , $K : = 0$ , $Λ : = 0$ , $κ > 0$ and the vacuum sector of Existence and uniqueness of the smooth maximal globally hyperbolic development of constrained initial data in the selected matter sectors (no matter fields, $T = 0$ ); the constraint equations reduce to $0 = 0$ and are satisfied. Then the maximal development of these data is, up to a unique data-fixing isometry, four-dimensional Minkowski spacetime $(R^{4}, η) = (R^{1, 3}, η)$ with the standard initial embedding $j : Σ \to R^{1, 3}$ , $j (x) = (0, x)$ , and time orientation $N = \partial_{t}$ .

Facts & Assumptions

Given: Countable Choice and Dependent Choice; the flat vacuum initial data $Σ : = R^{3}$ , $h : = δ$ , $K : = 0$ , $Λ : = 0$ , $κ > 0$ (no matter fields), and Minkowski spacetime $M : = (R^{1, 3}, η)$ with the embedding $j (x) = (0, x)$ and time orientation $\partial_{t}$ .

[L1]

Under Countable Choice and Dependent Choice, the maximal-development theorem Existence and uniqueness of the smooth maximal globally hyperbolic development of constrained initial data in the selected matter sectors requires connected smooth constrained complete data of one fixed admissible model, an existing development, and local existence and geometric uniqueness for that same model at every actual spacelike restart. Its conclusion gives a connected maximal development, an embedding of every development, and exactly one data-fixing isometry between maximal developments. For the present vacuum model, High-regularity local developments for the selected matter sectors: vacuum with Lambda, scalar, strict barotropic fluid and geodesic dust branch 1 supplies local existence and uniqueness for any smooth vacuum constraint data. Data induced on a smooth spacelike restart of a vacuum solution satisfy these same constraints by Gauss-Codazzi decomposition in Gaussian normal coordinates and the constraint equations in terms of the induced metric and second fundamental form. There are no matter variables, so initialization, matter reconstruction and conservation introduce no extra matter condition; the metric reduction is the supplied vacuum reduction. Step 1.1 below supplies the existing development. A data-fixing isometric immersion of developments is a development embedding by A data-fixing isometric immersion of developments is injective, hence a development embedding; uniqueness of data-fixing embeddings clause (b).

[L2]

The constant components of $η = - d t^{2} + \sum_{i = 1}^{3} (d x^{i})^{2}$ imply zero Christoffel symbols and curvature by A chart with constant metric components has vanishing metric-selected Christoffel symbols and curvature clauses (a)-(b). The geodesic equation of Coordinate geodesic equation therefore reduces to ${\ddot{x}}^{a} = 0$ : for any $p, v \in R^{4}$ , $s \mapsto p + s v$ is a geodesic for all $s \in R$ , and uniqueness in The geodesic initial-value problem and the exponential map of the metric-selected connection clause (a) makes it the maximal geodesic of those data. Local isometries preserve these geodesics by Rigidity of isometric immersions of a connected Lorentzian manifold, and agreement of data-fixing embeddings on overlaps step 1.1. The slice ${t = 0}$ is a Cauchy hypersurface by The flat model is globally hyperbolic and its inertial level sets are Cauchy hypersurfaces clause (b), and maximal timelike geodesics of any development are inextendible by Convergent causal ends are extendible, maximal geodesics have no limit, and Cauchy sets are acausal clause (b).

Verification

1.1givenL2algebra

(Minkowski is a development of the data.) On $R^{1, 3}$ with $η = - d t^{2} + δ$ the curvature vanishes, so the Einstein tensor vanishes and $G + Λ η = 0 = κ \cdot 0$ : the vacuum field equation holds by [L2]. The slice ${t = 0}$ is a spacelike embedded hypersurface with induced metric $δ$ and vanishing second fundamental form, since the unit normal $\partial_{t}$ is parallel; and every inextendible causal curve in $R^{1, 3}$ meets ${t = 0}$ exactly once, by The flat model is globally hyperbolic and its inertial level sets are Cauchy hypersurfaces: its time coordinate is strictly increasing and has range all of $R$ . Hence $(R^{1, 3}, η, \partial_{t}, j)$ is a development of the data.

2.1step 1.1L1L2algebra∎

(Completeness makes the embedding onto.) The connected initial manifold $R^{3}$ , the vacuum constraints, the existing development of step 1.1 and the restart obligations checked in [L1] satisfy the maximal theorem. Let $Q$ be its connected maximal development, and let $Φ : M \to Q$ be its data-fixing embedding of the Minkowski development from step 1.1. Fix $q \in Q$ and a maximal timelike geodesic through it. By Convergent causal ends are extendible, maximal geodesics have no limit, and Cauchy sets are acausal clause (b) this curve is inextendible and meets the initial Cauchy surface at some parameter $a$ . At that crossing, $Φ$ has invertible differential and fixes the initial embedding. Lift the crossing velocity to $M$ . The Minkowski geodesic with that initial datum is the straight line, defined for every affine parameter by A chart with constant metric components has vanishing metric-selected Christoffel symbols and curvature and The geodesic initial-value problem and the exponential map of the metric-selected connection. Its $Φ$ -image is a geodesic of $Q$ with the same crossing value and velocity; uniqueness makes it agree with the original geodesic on its entire interval, in particular at $q$ . Thus every $q$ lies in $Φ (M)$ , and the embedding is onto, hence a data-fixing isometry. Maximality and unique data-fixing isometry of $Q$ transfer to Minkowski. This proves the full claimed maximality, rather than inferring it solely from existence of an embedding.

Remarks

The example verifies the abstract maximality statement on a case in which every object is explicit; it also shows that "maximal" does not mean "complete": the maximal development of the flat vacuum data is complete, but the maximal development of other data need not be (Scope and empirical qualifications of the maximal globally hyperbolic development: model content, idealisations, and no observational claims). The verification uses the cited uniqueness theorem for the universal property and the flatness of $η$ for the development axioms; no claim about observations is made.

Depends on

Dependency tree · 2 levels

Sources

J. Sbierski, On the Existence of a Maximal Cauchy Development for the Einstein Equations - a Dezornification, arXiv:1309.7591v3 (2015): Theorem 2.8, whose flat vacuum instance is the example discussed here, printed pp. 12 and 20-24