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

A flat metric with nowhere-zero Christoffel coefficients: flat space in cylindrical coordinates

Example

On the open set $Ω : = {x \in R^{4} : x^{1} > 0}$ with the identity chart $x = (x^{0}, x^{1}, x^{2}, x^{3})$ consider the metric $g : = - (d x^{0})^{2} + (d x^{1})^{2} + (x^{1})^{2} (d x^{2})^{2} + (d x^{3})^{2}, N : = \partial_{0},$ and let $\nabla$ be its metric-selected connection and $R$ its curvature (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model, Metric compatibility, torsion freedom and the metric-selected connection class, Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields, The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors). Writing $X : = x^{1} \cos x^{2}$ and $Y : = x^{1} \sin x^{2}$ , the chain rule gives $d X = \cos x^{2} d x^{1} - x^{1} \sin x^{2} d x^{2}$ and $d Y = \sin x^{2} d x^{1} + x^{1} \cos x^{2} d x^{2}$ , hence $d X^{2} + d Y^{2} = (d x^{1})^{2} + (x^{1})^{2} (d x^{2})^{2}$ : the displayed metric is the flat metric $- (d x^{0})^{2} + d X^{2} + d Y^{2} + (d x^{3})^{2}$ pulled back by the map $(x^{0}, x^{1}, x^{2}, x^{3}) \mapsto (x^{0}, X, Y, x^{3})$ . This map is a local diffeomorphism on all of $Ω$ , so the metric is locally the flat Minkowski metric. It is not globally injective because $x^{2} \in R$ is an unwrapped angular coordinate; on every restriction where $x^{2}$ ranges over an interval of length less than $2 π$ , it gives genuine cylindrical coordinates. The component verification below uses only the displayed metric.

The only nonzero Christoffel symbols of $\nabla$ in this chart are $Γ^{1}_{22} = - x^{1}, Γ^{2}_{12} = Γ^{2}_{21} = \frac{1}{x^{1}},$ so these three coefficients are nonzero at every point of $Ω$ , while all other Christoffel symbols vanish identically.
The curvature vanishes identically, $R = 0$ , even though the chart has nonvanishing Christoffel symbols everywhere.
Consequently $R (T, J) T = 0$ for every geodesic tangent $T$ and every field $J$ along it: for every smooth family of affinely parametrized geodesics the deviation equation reads $D_{s}^{2} J = 0$ , with no tidal term.

Facts & Assumptions

Given: The open set $Ω = {x^{1} > 0} \subseteq R^{4}$ with the identity chart, the metric $g = diag (- 1, 1, (x^{1})^{2}, 1)$ , its metric-selected connection $\nabla$ and curvature $R$ .

[L1]

The metric $g$ is a smooth Lorentzian metric of signature $(-, +, +, +)$ on $Ω$ with time orientation $N = \partial_{0}$ , and $\nabla$ exists, is unique, and has Christoffel symbols $Γ^{a}_{b c} = \frac{1}{2} g^{a d} (\partial_{b} g_{d c} + \partial_{c} g_{b d} - \partial_{d} g_{b c})$ in the identity chart, with $g^{a d}$ the matrix inverse of $g_{a b}$ (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model, Metric compatibility, torsion freedom and the metric-selected connection class, Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields clause (a), Christoffel symbols of an affine connection, The inverse metric, musical isomorphisms and index raising).

[L2]

The curvature components in a chart are $R^{a}_{b c d} = \partial_{c} Γ^{a}_{d b} - \partial_{d} Γ^{a}_{c b} + \sum_{e} (Γ^{a}_{c e} Γ^{e}_{d b} - Γ^{a}_{d e} Γ^{e}_{c b})$ (Tensoriality of the curvature, its coordinate formula and its point-normal metric formula clause (b), The Riemann curvature operator and the derived Ricci, scalar and Einstein tensors clause (b)).

[L3]

The curvature is antisymmetric in the loop indices: $R^{a}_{b c d} = - R^{a}_{b d c}$ (The algebraic symmetries of the curvature tensor and the symmetry of the Ricci and Einstein tensors clause (a)).

[L4]

For a smooth family $F$ of affinely parametrized geodesics with $T = \partial_{t} F$ and $J = \partial_{r} F$ , the deviation equation $D_{t}^{2} J = R (T, J) T$ holds (The Jacobi equation, geodesic deviation and the initial-value theory of Jacobi fields clause (b), Covariant derivative along a curve, Geodesic of an affine connection).

Verification

technique · direct

1.1L1algebra

(Christoffel symbols.) In the identity chart only $g_{22} = (x^{1})^{2}$ is nonconstant, with $\partial_{1} g_{22} = 2 x^{1}$ , and $g^{22} = (x^{1})^{- 2}$ ; by [L1] the possible nonzero symbols are therefore $Γ^{1}_{22} = \frac{1}{2} g^{11} (- \partial_{1} g_{22}) = - x^{1}$ , $Γ^{2}_{12} = Γ^{2}_{21} = \frac{1}{2} g^{22} \partial_{1} g_{22} = 1 / x^{1}$ , and every other symbol has a factor $\partial_{a} g_{b c}$ with $a \neq 1$ or a constant metric component and vanishes. All displayed symbols are nonzero on all of $Ω$ because $x^{1} > 0$ there.

2.1L2step 1.1L3algebra

(Vanishing outside a finite list.) Let $a, b, c, d \in {0, 1, 2, 3}$ . Each of the four terms of [L2] contains a factor $Γ^{a}_{\cdot \cdot}$ , so $R^{a}_{b c d} = 0$ unless $a \in {1, 2}$ . If $c \notin {1, 2}$ then $c \in {0, 3}$ : the first term vanishes because $Γ^{a}_{d b}$ depends on $x^{1}$ alone, so $\partial_{0}$ and $\partial_{3}$ annihilate it; the second and fourth vanish because they contain $Γ^{a}_{c b}$ or $Γ^{e}_{c b}$ , whose lower index pair contains $c \notin {1, 2}$ ; the third vanishes because $Γ^{a}_{c e} = 0$ . If $d \notin {1, 2}$ : the first and third terms contain $Γ^{a}_{d b}$ or $Γ^{e}_{d b}$ with $d \notin {1, 2}$ and vanish, the second vanishes because $\partial_{d} Γ^{a}_{c b} = 0$ , and the fourth contains $Γ^{a}_{d e} = 0$ . Hence $R^{a}_{b c d}$ can be nonzero only when $a \in {1, 2}$ and $c, d \in {1, 2}$ ; by [L3] it then suffices to check the eight components $R^{a}_{b 12}$ with $a \in {1, 2}$ and $b \in {0, 1, 2, 3}$ .

2.2L2step 1.1algebra

(Components with a lower index outside the block.) Let $b \notin {1, 2}$ . In $R^{a}_{b 12}$ the first term is $\partial_{1} Γ^{a}_{2 b} = 0$ and the second is $\partial_{2} Γ^{a}_{1 b} = 0$ because both symbols have the lower index $b \notin {1, 2}$ ; the third term contains $Γ^{e}_{2 b} = 0$ and the fourth contains $Γ^{e}_{1 b} = 0$ for the same reason. Hence $R^{a}_{b 12} = 0$ for $b \in {0, 3}$ and $a \in {1, 2}$ .

3.1step 2.1step 2.2L2algebra

(The four remaining components.) By steps 2.1 and 2.2 only $R^{1}_{112}$ , $R^{1}_{212}$ , $R^{2}_{112}$ and $R^{2}_{212}$ remain. Term by term, $Γ^{1}_{1 e} = 0$ for all $e$ and $Γ^{e}_{11} = 0$ for all $e$ , so the middle products vanish in the surviving components and $R^{1}_{112} = 0$ : using step 1.1 and the fourth term $- Γ^{1}_{2 e} Γ^{e}_{12}$ with $e = 2$ , $R^{1}_{212} = \partial_{1} Γ^{1}_{22} - \partial_{2} Γ^{1}_{12} - 0 - Γ^{1}_{22} Γ^{2}_{12} = - 1 + (- x^{1}) (- \frac{1}{x^{1}}) = 0$ and $R^{2}_{112} = \partial_{1} Γ^{2}_{21} - \partial_{2} Γ^{2}_{11} + Γ^{2}_{12} Γ^{2}_{21} - 0 = - \frac{1}{(x^{1})^{2}} + \frac{1}{(x^{1})^{2}} = 0,$ while every term of $R^{1}_{112}$ and of $R^{2}_{212}$ contains a vanishing symbol, so those two components are $0$ as well.

4.1step 1.1step 3.1L4given∎

(Conclusion and consequence.) Steps 2.1, 2.2 and 3.1 show that every component $R^{a}_{b c d}$ vanishes at every point of $Ω$ , so $R = 0$ , although step 1.1 shows that the Christoffel symbols do not vanish anywhere. Nonvanishing connection coefficients in curvilinear coordinates are chart artifacts, not curvature: no coordinate-invariant conclusion can be drawn from them. By [L4], for every smooth family $F$ of affinely parametrized geodesics the variation field satisfies $D_{s}^{2} J = R (T, J) T = 0$ : the congruence has no tidal term, and its deviation is governed only by the affine initial data.

Remarks

The metric is flat and the identity chart on $Ω$ is not a point-normal chart at any point: its three displayed Christoffel coefficients are nonzero everywhere, while every other coefficient is zero. The vanishing of Christoffel symbols is therefore a property of a chart at a point and not a property of the geometry; only the curvature computed above, which is the second-order chart-independent information (Tensoriality of the curvature, its coordinate formula and its point-normal metric formula clause (a)), can detect the difference between flat space and a genuinely curved spacetime.

A flat metric with nowhere-zero Christoffel coefficients: flat space in cylindrical coordinates

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources