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

Worked example: splitting a four-velocity in an observer's rest frame

Example

Worked computation. In an inertial chart with $η_{0} = diag (- 1, 1, 1, 1)$ let the observer be $n = e_{0} = (1, 0, 0, 0)$ and let $u = (5 / 4, 3 / 4, 0, 0)$ , a future unit timelike vector: $η (u, u) = - 25 / 16 + 9 / 16 = - 1$ . Then $γ = - η (n, u) = 5 / 4 \geq 1$ , $h (u) = u + η (n, u) n = u - (5 / 4) (1, 0, 0, 0) = (0, 3 / 4, 0, 0)$ lies in $n^{⊥} = span (e_{1}, e_{2}, e_{3})$ , and the relative velocity is $w = c h (u) / γ = (0, 3 c / 5, 0, 0)$ . One checks $u = γ (n + w / c) = (5 / 4) (1, 3 / 5, 0, 0)$ and $∣ w ∣^{2} = 9 c^{2} / 25 = c^{2} (1 - γ^{- 2}) = c^{2} (1 - 16 / 25)$ . Also $h (h (u)) = h (u)$ and $η (n, h (u)) = 0$ . This four-velocity is the one of the clock with coordinate velocity $(3 c / 5, 0, 0)$ in Worked example: proper time and four-velocity of a straight worldline at beta = 3/5.

Facts & Assumptions

Given: An inertial chart with $η_{0} = diag (- 1, 1, 1, 1)$ , the observer $n = e_{0} = (1, 0, 0, 0)$ and the vector $u = (5 / 4, 3 / 4, 0, 0)$ .

[L1]

Decomposition (Norms of four-velocity and four-acceleration, and the observer rest-space decomposition): for future unit timelike $n, u$ the projection is $h (v) = v + η (n, v) n$ with image $n^{⊥}$ and $h \circ h = h$ and $η (n, h (v)) = 0$ ; $γ = - η (n, u) \geq 1$ , $w = c h (u) / γ \in n^{⊥}$ , $u = γ (n + w / c)$ , $∣ w ∣^{2} = c^{2} (1 - γ^{- 2}) < c^{2}$ , and $γ = 1 ⟺ u = n$ .

[L2]

Chart (Inertial frames and inertial charts of the affine Minkowski model, The Euclidean spatial structure and cross product of an inertial frame): the chart's observer is $e_{0}$ , and $n^{⊥} = span (e_{1}, e_{2}, e_{3})$ is the Euclidean spatial space of the frame with $∣ w ∣ = \sqrt{δ (w, w)}$ .

[L3]

Bilinearity (Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space): in the chart, $η (v, z) = - v^{0} z^{0} + v^{1} z^{1} + v^{2} z^{2} + v^{3} z^{3}$ .

[L4]

Observer clause (Four-velocity and four-acceleration of a future timelike worldline): the four-velocity of the observer's own worldline with future unit timelike $n$ is $c n$ .

Verification

technique · direct

1.1givenL1L3

By [L3], $η (u, u) = - 25 / 16 + 9 / 16 = - 1$ and $η (n, n) = - 1$ , so both $n$ and $u$ are unit timelike; both are future because their first coordinates are positive and $u^{0} = 5 / 4 > ∣ u_{s p} ∣ = 3 / 4$ , $n^{0} = 1 > 0$ ; hence [L1] applies.

2.1step 1.1L1L3

Direct computation in the chart: $γ = - η (n, u) = 5 / 4$ , and $h (u) = u + η (n, u) n = u - (5 / 4) (1, 0, 0, 0) = (0, 3 / 4, 0, 0)$ .

3.1step 2.1L1L2L3

The vector $h (u) = (0, 3 / 4, 0, 0)$ lies in $span (e_{1}, e_{2}, e_{3}) = n^{⊥}$ by [L2], and $η (n, h (u)) = - 1 \cdot 0 + 0 = 0$ by [L3]; idempotence $h (h (u)) = h (u)$ holds because $h (u) \in n^{⊥}$ is fixed by $h$ by [L1].

4.1step 2.1step 3.1L1L2

The relative velocity is $w = c h (u) / γ = (0, 3 c / 5, 0, 0)$ with $∣ w ∣^{2} = 9 c^{2} / 25$ by [L2]; the split identity gives $u = γ (n + w / c) = (5 / 4) (1, 3 / 5, 0, 0) = (5 / 4, 3 / 4, 0, 0)$ and the Lorentz-factor identity $∣ w ∣^{2} = c^{2} (1 - γ^{- 2}) = c^{2} (1 - 16 / 25) = 9 c^{2} / 25$ , both by [L1].

5.1step 4.1L1L4∎

By [L4] the observer's four-velocity is $c n = (c, 0, 0, 0)$ ; since $γ = 5 / 4 \neq 1$ , the criterion of [L1] gives $u \neq n$ , so the clock's four-velocity $c u$ differs from the observer's and the split is nondegenerate.

Remarks

The split is algebraic, not dynamic. The computation uses only the projection $h$ , the inner product and the definitions of $γ$ and $w$ ; no differentiation, no dynamics and no physical measurement is involved.
Companion clock. The dimensionless four-velocity $u = (5 / 4, 3 / 4, 0, 0)$ is the one of the straight clock with coordinate velocity $(3 c / 5, 0, 0)$ worked out in Worked example: proper time and four-velocity of a straight worldline at beta = 3/5; the split above re-derives that clock's relative velocity without using its worldline.

Worked example: splitting a four-velocity in an observer's rest frame

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels