ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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 constant boosted tetrad field on flat spacetime and an adapted chart

Example

Let $M = R^{4}$ carry the identity chart $x = (x^{0}, x^{1}, x^{2}, x^{3})$ and the flat Lorentzian metric $g = diag (- 1, 1, 1, 1)$ , with time orientation $N = \partial_{0}$ . Let $β \in (- 1, 1)$ and let $γ : = (1 - β^{2})^{- 1 / 2} > 0$ . Define the constant-coefficient fields

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

Then $(E_{0}, E_{1}, E_{2}, E_{3})$ is a smooth future-directed tetrad field on $M$ , and $n : = E_{0}$ is an observer congruence whose integral curves have $x^{1} - β x^{0}$ , $x^{2}$ and $x^{3}$ constant; hence $u : = (x^{0}, x^{1} - β x^{0}, x^{2}, x^{3})$ is an $n$ -adapted chart. In that chart $n = γ \partial_{u^{0}}$ , so the coordinate field of an adapted chart need not equal the congruence.

Facts & Assumptions

Given: The flat Lorentzian four-manifold $(R^{4}, g)$ with identity chart $x$ , time orientation $N = \partial_{0}$ , parameter $β \in (- 1, 1)$ and $γ = (1 - β^{2})^{- 1 / 2}$ .

[L1]

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

[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, and it is future-directed when $E_{0}$ is future-directed at every point (Local frame fields, coordinate frames and tetrad fields).

[L3]

A vector field on a chart domain is smooth exactly when its coordinate components are smooth; constant components are smooth (Smoothness of a vector field is equivalent to smooth coordinate components).

[L4]

An observer congruence on an open set is a smooth field $n$ with $g_{q} (n_{q}, n_{q}) = - 1$ whose values are future-directed; 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).

Verification

technique · direct

1.1givenL3

The fields $E_{0}, E_{1}, E_{2}, E_{3}$ have constant coordinate components by their definition, so they are smooth vector fields on $R^{4}$ by [L3].

2.1step 1.1L2algebra

Evaluating the flat metric on the constant fields gives $g (E_{0}, E_{0}) = γ^{2} (- 1 + β^{2}) = - 1$ , $g (E_{1}, E_{1}) = γ^{2} (- β^{2} + 1) = 1$ , $g (E_{0}, E_{1}) = γ^{2} (- β + β) = 0$ , $g (E_{2}, E_{2}) = g (E_{3}, E_{3}) = 1$ and all remaining pairings $0$ because the fields involve only the $\partial_{0}, \partial_{1}$ directions or are the orthonormal fields $\partial_{2}, \partial_{3}$ . Hence $g (E_{A}, E_{B}) = diag (- 1, 1, 1, 1)_{A B}$ pointwise, and the tuple is an ordered basis at every point; it is a tetrad field by [L2].

3.1step 2.1L1L2algebra

The first member satisfies $g (E_{0}, N) = g (E_{0}, \partial_{0}) = - γ < 0$ , so $E_{0}$ is future-directed by [L1] and $(E_{0}, E_{1}, E_{2}, E_{3})$ is a future-directed tetrad field.

4.1step 3.1L4algebra

The field $n : = E_{0} = γ (\partial_{0} + β \partial_{1})$ is a smooth future unit timelike field, hence an observer congruence by [L4]. Its integral curves satisfy ${\dot{x}}^{0} = γ$ , ${\dot{x}}^{1} = γ β$ , ${\dot{x}}^{2} = {\dot{x}}^{3} = 0$ , so $x^{2}$ and $x^{3}$ are constant and $\frac{d}{d s} (x^{1} - β x^{0}) = γ β - β γ = 0$ ; therefore $x^{1} - β x^{0}$ , $x^{2}$ and $x^{3}$ are constant along every integral curve.

5.1step 4.1L4algebra∎

The map $u = (u^{0}, u^{1}, u^{2}, u^{3}) : = (x^{0}, x^{1} - β x^{0}, x^{2}, x^{3})$ has the smooth inverse $x^{0} = u^{0}$ , $x^{1} = u^{1} + β u^{0}$ , $x^{2} = u^{2}$ , $x^{3} = u^{3}$ , so it is a chart, and by step 4.1 its spatial coordinates $u^{1}, u^{2}, u^{3}$ are constant along the integral curves of $n$ ; the chart is $n$ -adapted by [L4]. In these coordinates $\partial_{u^{0}} = \partial_{0} + β \partial_{1} = n / γ$ , so $n = γ \partial_{u^{0}}$ . It equals $\partial_{u^{0}}$ exactly when $β = 0$ (then $γ = 1$ ), and differs when $β \neq 0$ ; thus an adapted chart need not have the congruence as its coordinate field. No uniqueness of adapted charts is claimed.

Remarks

The example shows that an adapted chart exists for this congruence and that its coordinate time need not be the flow parameter of $n$ ; the existence corollary on the tensors page produces a different adapted chart in which $n = \partial_{u^{0}}$ exactly. The congruence is parallel in the identity chart, so its observers are straight lines; no curvature or acceleration claim is made.

A constant boosted tetrad field on flat spacetime and an adapted chart

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources