ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

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: proper time and four-velocity of a straight worldline at beta = 3/5

Example

Worked computation. In an inertial chart with $η_{0} = diag (- 1, 1, 1, 1)$ let $c > 0$ and, for $t \in R$ , consider the coordinate worldline $x (t) = (c t, (3 c / 5) t, 0, 0)$ , parametrized by coordinate time, which describes a clock moving along the first spatial axis with speed $3 c / 5$ . Then $x^{'} (t) = (c, 3 c / 5, 0, 0)$ and $η (x^{'}, x^{'}) = - c^{2} + (9 / 25) c^{2} = - (16 / 25) c^{2}$ , so $\sqrt{- η (x^{'}, x^{'})} = 4 c / 5$ and $τ (t) - τ (t_{0}) = (4 / 5) (t - t_{0})$ : the moving clock runs slow by the factor $4 / 5 = 1 / γ$ with $γ = 5 / 4$ . The four-velocity is $U = x^{'} / τ^{'} = (5 / 4) (c, 3 c / 5, 0, 0) = (5 c / 4, 3 c / 4, 0, 0)$ , which satisfies $η (U, U) = - 25 c^{2} / 16 + 9 c^{2} / 16 = - c^{2}$ , and the four-acceleration vanishes because $U$ is constant: $A = 0$ . The dimensionless four-velocity is $u = U / c = (5 / 4, 3 / 4, 0, 0)$ ; the split of clause (d) with $n = e_{0}$ gives $γ = 5 / 4$ and relative velocity $w = (0, 3 c / 5, 0, 0) \in e_{0}^{⊥}$ , whose spatial coordinates are exactly the coordinate velocity.

Facts & Assumptions

Given: An inertial chart with $η_{0} = diag (- 1, 1, 1, 1)$ a real $c > 0$ , and the worldline $x : R \to A$ with coordinates $x (t) = (c t, (3 c / 5) t, 0, 0)$ .

[L1]

Inertial charts (Inertial frames and inertial charts of the affine Minkowski model): in an inertial chart the matrix of $η$ is $diag (- 1, 1, 1, 1)$ and the chart's observer is $e_{0}$ .

[L2]

Curves (Curves, regular causal curves and future timelike worldlines in affine Minkowski space): the difference quotients of $x$ are identically $(c, 3 c / 5, 0, 0)$ , so $x^{'} (t) = (c, 3 c / 5, 0, 0)$ ; the sign of $η (x^{'}, x^{'})$ decides the causal character (Timelike, null, spacelike and causal vectors of a Lorentz vector space).

[L3]

Proper time (Proper time along a future timelike worldline): for a constant tangent $x^{'}$ the increment is $c^{- 1} (t - t_{0}) \sqrt{- η (x^{'}, x^{'})}$ .

[L4]

Four-velocity and four-acceleration (Four-velocity and four-acceleration of a future timelike worldline): $U = x^{'} / τ^{'}$ , and $A = U^{'} / τ^{'}$ when $x$ is $C^{2}$ ; a constant $U$ has zero derivative.

[L5]

Decomposition (Norms of four-velocity and four-acceleration, and the observer rest-space decomposition): clauses (a), (c), (d): $η (U, U) = - c^{2}$ ; for the observer $e_{0}$ , $γ = - η (e_{0}, u)$ and the relative velocity is $w = c h (u) / γ = (0, w_{s p})$ when $u = γ_{w} (c, w) / c$ .

[L6]

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

Verification

technique · direct

1.1givenL1L2L6

The difference quotients of $x$ are identically $(c, 3 c / 5, 0, 0)$ , so $x^{'} (t) = (c, 3 c / 5, 0, 0)$ ; by [L6], $η (x^{'}, x^{'}) = - c^{2} + 9 c^{2} / 25 = - (16 / 25) c^{2} < 0$ , so $x$ is a $C^{1}$ future timelike worldline by [L2].

2.1step 1.1L3

By [L3] the proper-time increment is $τ (t) - τ (t_{0}) = c^{- 1} (t - t_{0}) \cdot (4 c / 5) = (4 / 5) (t - t_{0})$ , so the moving clock's proper time runs at the rate $4 / 5 = 1 / γ$ with $γ = 5 / 4$ .

3.1step 1.1step 2.1L4L5L6

The four-velocity is $U = x^{'} / τ^{'} = (5 / 4) (c, 3 c / 5, 0, 0) = (5 c / 4, 3 c / 4, 0, 0)$ ; it is constant, so $A = U^{'} / τ^{'} = 0$ by [L4]; and $η (U, U) = - 25 c^{2} / 16 + 9 c^{2} / 16 = - c^{2}$ by [L6], in agreement with clause (a) of [L5].

4.1step 3.1L5∎

The dimensionless four-velocity is $u = U / c = (5 / 4, 3 / 4, 0, 0)$ with $η (u, u) = - 1$ ; the split of clause (d) of [L5] with $n = e_{0}$ gives $γ = - η (e_{0}, u) = 5 / 4$ , $h (u) = u - u^{0} e_{0} = (0, 3 / 4, 0, 0)$ and relative velocity $w = c h (u) / γ = (0, 3 c / 5, 0, 0)$ , whose spatial coordinates are exactly the coordinate velocity of the worldline; the Lorentz-factor identity $∣ w ∣^{2} = c^{2} (1 - γ^{- 2}) = c^{2} (1 - 16 / 25) = 9 c^{2} / 25$ holds.

Remarks

All numbers are exact rationals. The computation uses only the diagonal form of $η$ and the rational values $3 / 5$ , $4 / 5$ , $5 / 4$ ; no numerical approximation and no measurement is involved.
The factor $1 / γ$ is a model statement. That the moving ideal clock runs slow by $4 / 5$ is a statement about the model's proper time, not a reported measurement of any physical clock.

Worked example: proper time and four-velocity of a straight worldline at beta = 3/5

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels