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 shearing observer congruence on flat spacetime: tetrad, adapted chart and non-coordinate frame

Example

Let $M = R^{4}$ carry the identity chart $x$ and the flat Lorentzian metric $g = diag (- 1, 1, 1, 1)$ with time orientation $N = \partial_{0}$ . Fix $λ > 0$ and put

$W : = {(x^{0}, x^{1}, x^{2}, x^{3}) : ∣ λ x^{1} ∣ < 1 / 2}, Ω : = λ x^{1}, γ : = (1 - Ω^{2})^{- 1 / 2} > 0.$

Define the smooth fields on $W$

$E_{0} : = γ (\partial_{0} + Ω \partial_{2}), E_{1} : = \partial_{1}, E_{2} : = γ (Ω \partial_{0} + \partial_{2}), E_{3} : = \partial_{3} .$

Then $(E_{0}, E_{1}, E_{2}, E_{3})$ is a future-directed tetrad field on $W$ , its first member $n : = E_{0}$ is an observer congruence, the chart $u : = (x^{0}, x^{1}, x^{2} - Ω (x^{1}) x^{0}, x^{3})$ is $n$ -adapted with $\partial_{u^{0}} = n / γ$ , and the tetrad is not the coordinate frame of any chart, because $[E_{0}, E_{1}] = - γ^{'} \partial_{0} - (γ Ω)^{'} \partial_{2}$ is nonzero at every point of $W$ with $x^{1} \neq 0$ , where $γ^{'} = γ^{3} λ^{2} x^{1}$ .

Facts & Assumptions

Given: The flat Lorentzian four-manifold $(R^{4}, g)$ with identity chart $x$ , time orientation $N = \partial_{0}$ , parameters $λ > 0$ , $Ω = λ x^{1}$ , $γ = (1 - Ω^{2})^{- 1 / 2}$ on the open set $W = {∣ Ω ∣ < 1 / 2}$ , and the four fields $E_{0}, E_{1}, E_{2}, E_{3}$ .

[L1]

On $R^{4}$ with the flat metric the coordinate fields satisfy $g (\partial_{a}, \partial_{b}) = diag (- 1, 1, 1, 1)_{a b}$ , and a nonzero causal vector is future-directed exactly when $g (v, N) < 0$ (Smooth time-oriented Lorentzian four-manifolds: the geometric objects of the model).

[L2]

A tetrad field on an open set is a tuple of four pointwise independent smooth vector fields with $g (E_{A}, E_{B}) = diag (- 1, 1, 1, 1)_{A B}$ pointwise; the coordinate frame of a chart has pairwise commuting members, so a frame with some nonvanishing bracket is not the coordinate frame of any chart (Local frame fields, coordinate frames and tetrad fields).

[L3]

An observer congruence on an open set is a smooth field $n$ with $g (n, n) = - 1$ and future-directed values; a chart is $n$ -adapted when its spatial coordinates are constant along every integral curve of $n$ (Observer congruences, their observer curves and adapted charts).

[L4]

A vector field is smooth exactly when its coordinate components are smooth (Smoothness of a vector field is equivalent to smooth coordinate components).

[L5]

Finite sums, products and composites of $C^{\infty}$ functions are $C^{\infty}$ on their domains ( $C^{k}$ Euclidean maps are closed under componentwise algebra and composition).

[L6]

The squaring map $u \mapsto u^{2}$ is injective on $(0, \infty)$ with derivative $2 u \neq 0$ there, so by the injective-regular-map theorem its inverse $u \mapsto u^{1 / 2}$ is $C^{\infty}$ on $(0, \infty)$ ; the reciprocal $u \mapsto u^{- 1}$ is $C^{\infty}$ on $(0, \infty)$ by the iterated product and quotient rules (An injective regular $C^{k}$ map is a $C^{k}$ diffeomorphism onto its image, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[L7]

In a chart, $[X, Y] = \sum_{j} (\sum_{i} X^{i} \partial_{i} Y^{j} - Y^{i} \partial_{i} X^{j}) \partial_{j}$ (Coordinate formula for the Lie bracket).

Verification

technique · direct

1.1L5L6given

The set $W$ is open and $1 - Ω^{2} > 3 / 4 > 0$ on $W$ . By [L6] the function $u \mapsto u^{- 1 / 2}$ is $C^{\infty}$ on $(0, \infty)$ , so $γ$ is $C^{\infty}$ on $W$ as a composite with the polynomial $1 - Ω^{2}$ , and $Ω, γ, γ Ω$ are $C^{\infty}$ on $W$ by [L5].

2.1step 1.1L1L3L4algebra

The fields $E_{0}, \dots, E_{3}$ have $C^{\infty}$ components in the chart $x$ by step 1.1, hence are smooth vector fields on $W$ by [L4]. Moreover $g (n, n) = γ^{2} (- 1 + Ω^{2}) = - 1$ and $g (n, N) = g (γ (\partial_{0} + Ω \partial_{2}), \partial_{0}) = - γ < 0$ , so $n = E_{0}$ is future unit timelike; by [L3] it is an observer congruence on $W$ .

3.1step 2.1L2algebra

Evaluating $g$ on the fields gives: $g (E_{0}, E_{0}) = γ^{2} (- 1 + Ω^{2}) = - 1$ ; $g (E_{2}, E_{2}) = γ^{2} (Ω^{2} g (\partial_{0}, \partial_{0}) + g (\partial_{2}, \partial_{2})) = γ^{2} (1 - Ω^{2}) = 1$ ; $g (E_{0}, E_{2}) = γ^{2} (Ω g (\partial_{0}, \partial_{0}) + Ω g (\partial_{2}, \partial_{2})) = γ^{2} (- Ω + Ω) = 0$ ; $g (E_{1}, E_{1}) = g (E_{3}, E_{3}) = 1$ ; and every pairing involving $E_{1} = \partial_{1}$ or $E_{3} = \partial_{3}$ vanishes because $\partial_{1}, \partial_{3}$ are orthogonal to $\partial_{0}, \partial_{2}$ . Hence $g (E_{A}, E_{B}) = diag (- 1, 1, 1, 1)_{A B}$ pointwise, and the tuple is a tetrad field by [L2]; it is future-directed because $E_{0} = n$ is.

3.2step 2.1algebra

An integral curve of $n$ satisfies ${\dot{x}}^{0} = γ$ , ${\dot{x}}^{1} = 0$ , ${\dot{x}}^{2} = γ Ω$ , ${\dot{x}}^{3} = 0$ ; along such a curve $x^{1}$ is constant, so the values $γ$ , $Ω$ are constant on it, and therefore $x^{3}$ is constant and $\frac{d}{d s} (x^{2} - Ω x^{0}) = γ Ω - Ω γ = 0$ . Thus $x^{1}$ , $x^{3}$ and $x^{2} - Ω (x^{1}) x^{0}$ are constant along every integral curve.

4.1step 3.2L3algebra

The map $u = (u^{0}, u^{1}, u^{2}, u^{3}) : = (x^{0}, x^{1}, x^{2} - Ω (x^{1}) x^{0}, x^{3})$ has the explicit smooth inverse $x^{0} = u^{0}$ , $x^{1} = u^{1}$ , $x^{2} = u^{2} + Ω (u^{1}) u^{0}$ , $x^{3} = u^{3}$ on its image, so it is a chart; by step 3.2 its spatial coordinates are constant along the integral curves of $n$ , so the chart is $n$ -adapted by [L3]. In these coordinates $\partial_{u^{0}} = \partial_{0} + Ω \partial_{2} = n / γ$ , so the coordinate field of the adapted chart is $n / γ$ , not $n$ .

5.1step 4.1L2L7algebra∎

By [L7], the bracket of $E_{0} = γ \partial_{0} + γ Ω \partial_{2}$ and $E_{1} = \partial_{1}$ is $[E_{0}, E_{1}]^{j} = \sum_{i} (E_{0}^{i} \partial_{i} E_{1}^{j} - E_{1}^{i} \partial_{i} E_{0}^{j}) = - \partial_{1} E_{0}^{j}$ , so $[E_{0}, E_{1}] = - \partial_{1} (γ) \partial_{0} - \partial_{1} (γ Ω) \partial_{2} = - γ^{'} \partial_{0} - (γ Ω)^{'} \partial_{2}$ . Since $γ = (1 - Ω^{2})^{- 1 / 2}$ and $Ω = λ x^{1}$ , the chain and power rules give $γ^{'} = γ^{3} Ω Ω^{'} = γ^{3} λ^{2} x^{1}$ , which is nonzero at every point of $W$ with $x^{1} \neq 0$ ; hence $[E_{0}, E_{1}] \neq 0$ at such points. By the commuting necessary condition of [L2], the tetrad field is not the coordinate frame of any chart.

Remarks

The congruence is a shearing motion: its observers move in the $\partial_{2}$ direction with a speed $Ω$ that depends on $x^{1}$ . The example shows in one place that congruence, adapted chart, tetrad field and coordinate frame are four different objects: an adapted chart exists while the tetrad is not a coordinate frame, and the adapted chart does not have $n$ as a coordinate field. Integrability of the rest spaces of this congruence is decided by the separate counterexample on this page.

A shearing observer congruence on flat spacetime: tetrad, adapted chart and non-coordinate frame

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources