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.

The relative-velocity decomposition of a boost, checked in an explicit tetrad

Example

Let $(R^{4}, g)$ and the constant boosted tetrad field $(E_{0}, E_{1}, E_{2}, E_{3})$ be as in A constant boosted tetrad field on flat spacetime and an adapted chart, with $E_{0} = n$ future unit timelike, $E_{1}$ unit spacelike and $g (E_{0}, E_{1}) = 0$ . Let $β \in (- 1, 1)$ , $γ = (1 - β^{2})^{- 1 / 2}$ and $c > 0$ , and set

$w : = β c E_{1}, u : = γ (n + \frac{w}{c}) = γ (E_{0} + β E_{1}) .$

Then $u$ is future unit timelike, $- g (n, u) = γ \geq 1$ , $h_{n} (u) = γ β E_{1}$ , $w = c h_{n} (u) / γ$ , and $g (w, w) = β^{2} c^{2} = c^{2} (1 - γ^{- 2}) < c^{2}$ whenever $β \neq 0$ . This verifies the relative-velocity decomposition theorem of the tensors page in an explicit family.

Facts & Assumptions

Given: The constant boosted tetrad $(E_{0}, E_{1}, E_{2}, E_{3})$ on $R^{4}$ with flat metric $g$ , its first member $n = E_{0}$ , parameters $β \in (- 1, 1)$ , $γ = (1 - β^{2})^{- 1 / 2}$ , $c > 0$ , and the vectors $w = β c E_{1}$ , $u = γ (n + w / c)$ .

[L1]

The fields $E_{0} = γ (\partial_{0} + β \partial_{1})$ , $E_{1} = γ (β \partial_{0} + \partial_{1})$ satisfy $g (E_{0}, E_{0}) = - 1$ , $g (E_{1}, E_{1}) = 1$ , $g (E_{0}, E_{1}) = 0$ ; $n = E_{0}$ is future-directed; and $E_{2} = \partial_{2}$ , $E_{3} = \partial_{3}$ (A constant boosted tetrad field on flat spacetime and an adapted chart).

[L2]

If $n$ is an observer, $c > 0$ , $u$ is future unit timelike and $γ_{o} = - g (n, u)$ , $w_{o} = c h_{n} (u) / γ_{o}$ , then $γ_{o} \geq 1$ , $u = γ_{o} (n + w_{o} / c)$ and $g (w_{o}, w_{o}) = c^{2} (1 - γ_{o}^{- 2})$ (Relative velocity decomposition of a future unit timelike vector).

[L3]

An observer is a future-directed unit timelike vector; the spatial projection is $h_{n} (v) = v + g_{p} (n, v) n$ (Observers, rest spaces and the spatial projection at an event), 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).

Verification

technique · direct

1.1L1L3algebra

Since $g (n, n) = - 1$ , $g (E_{1}, E_{1}) = 1$ and $g (n, E_{1}) = 0$ by [L1], bilinearity gives $g (u, u) = γ^{2} (g (n, n) + 2 β g (n, E_{1}) + β^{2} g (E_{1}, E_{1})) = γ^{2} (- 1 + β^{2}) = - 1$ , so $u$ is unit timelike. Moreover $g (n, N) = g (E_{0}, \partial_{0}) = - γ$ and $g (E_{1}, \partial_{0}) = - γ β$ by [L1], so $g (u, N) = γ (g (n, N) + β g (E_{1}, N)) = - γ^{2} (1 + β^{2}) < 0$ ; by [L3] the vector $u$ is future-directed.

2.1step 1.1L1L3algebra

By [L3] and [L1], $h_{n} (u) = u + g (u, n) n = u - γ n = γ (E_{0} + β E_{1}) - γ E_{0} = γ β E_{1}$ . Moreover $g (u, n) = γ (g (n, n) + β g (E_{1}, n)) = - γ$ , since $g (n, E_{1}) = 0$ ; hence $γ_{o} : = - g (n, u) = γ$ and $w_{o} : = c h_{n} (u) / γ_{o} = c β E_{1} = w$ .

3.1step 1.1step 2.1L2algebra∎

The identities $u = γ (n + w / c)$ and $g (w, w) = β^{2} c^{2}$ hold by definition of $w$ and [L1]; since $γ^{- 2} = 1 - β^{2}$ , we have $g (w, w) = c^{2} (1 - γ^{- 2}) < c^{2}$ for $β \neq 0$ , while for $β = 0$ the vector $w$ vanishes and $u = n$ . Thus the explicit pair $(γ, w)$ is exactly the decomposition produced by [L2] for $u$ , and $γ \geq 1$ .

Remarks

The example is the flat-spacetime boost written in the abstract split of a single tetrad: no coordinate chart enters, and the only data are the observer $n$ , the spatial direction $E_{1}$ , the speed parameter $β$ and the conversion constant $c$ .

The relative-velocity decomposition of a boost, checked in an explicit tetrad

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources