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 worked Galilean boost: the same uniform motion in two inertial frames

Physical scope

A finite worked verification, on explicit numerical data, of the transformation law between two inertial frames of the model and of the velocity and acceleration laws for one uniform motion: checking adaptedness of a constructed frame, the coordinate relation, the parameter condition, and the transformation of coordinate and spatial velocity. It is a computation inside an explicitly specified model and asserts no force law, no empirical claim and no physical law beyond the cited items.

Example

Take the concrete model data

$V = R^{4}, τ (x^{0}, x^{1}, x^{2}, x^{3}) = x^{0}, K = {0} \times R^{3},$

with $g$ the standard Euclidean inner product $g ((0, u), (0, w)) = u \cdot w$ on $K$ , the standard orientation of $K$ , and $A = R^{4}$ with its standard affine structure over $V$ ; the coordinates are read with $t$ in seconds and $(x^{1}, x^{2}, x^{3})$ in metres. Adopt the spacetime, frame and worldline postulates (Adopted Newtonian spacetime structure: absolute time, Euclidean spatial slices and their smooth structure, Inertial frames, stationary observers and the adopted Galilean transformations between frames, Particle labels, worldlines, the frame-time parameter condition and fixed inertial masses).

First frame. $F = (o, u, (e_{1}, e_{2}, e_{3}))$ with $o = 0$ , $u = (1, 0, 0, 0)$ , $e_{1} = (0, 1, 0, 0)$ , $e_{2} = (0, 0, 1, 0)$ , $e_{3} = (0, 0, 0, 1)$ . The adapted coordinates are the standard ones, written $(t, x) = (t, x^{1}, x^{2}, x^{3})$ .

Transformation data. Choose

$b = 2 s, a = (0, 3 m, 0), v = (\frac{1}{2}, 0, 0) m s^{- 1}, R = I_{3} .$

Second frame constructed from the data. Put $e_{j}^{'} = e_{j}$ for $j = 1, 2, 3$ (the rotation is trivial), $u^{'} = u - \sum_{j} v_{j} e_{j}^{'} = (1, - \frac{1}{2}, 0, 0)$ and $o^{'} = o - b u - \sum_{j} (R^{T} (a - v b))_{j} e_{j} = (- 2, 1, - 3, 0)$ ; write $(t^{'}, x^{'})$ for the adapted coordinates of $F^{'} = (o^{'}, u^{'}, (e_{1}^{'}, e_{2}^{'}, e_{3}^{'}))$ .

The motion. Let $γ : R \to A$ be the worldline whose $F$ -coordinates are

$γ (s) = (s, 1 + \frac{1}{4} s, 2, 0),$

that is, the coordinate curve $x (s) = (1 + \frac{1}{4} s, 2, 0)$ with constant coordinate velocity $w = (\frac{1}{4}, 0, 0) m s^{- 1}$ and zero coordinate acceleration.

Facts & Assumptions

Given: The data $(V, τ, g, K, orientation, A)$ of the Example, the frames $F$ and $F^{'}$ , the worldline $γ$ with its $F$ -coordinate curve $x$ , and the primed coordinate curve $η (t^{'}) = x^{'} (γ (t^{'} - b))$ of Coordinate velocity and acceleration of a worldline in an inertial frame, and the spatial velocity and acceleration vectors.

[L1]

The Newtonian spacetime postulate: $V$ a four-dimensional real vector space, $τ$ surjective linear with kernel $K$ of dimension three, $g$ a positive-definite bilinear form on $K$ , a fixed orientation of $K$ and an affine space $A$ modelled on $V$ (Adopted Newtonian spacetime structure: absolute time, Euclidean spatial slices and their smooth structure, Affine time space with Euclidean simultaneous slices and adapted charts).

[L2]

Inertial frames are the adapted charts $(o, u, (e_{j}))$ with $τ (u) = 1$ and $(e_{j})$ an oriented $g$ -orthonormal basis of $K$ (Inertial frames, stationary observers and the adopted Galilean transformations between frames).

[L3]

The Galilean kinematics theorem: the transformation law between inertial frames, the velocity law $η^{'} (t^{'}) = R w (t^{'} - b) + v$ , the acceleration law $η^{''} (t^{'}) = R α (t^{'} - b)$ with $α : = x^{''}$ , and the frame-independence of vanishing coordinate acceleration (Galilean transformation of worldlines: velocity and acceleration laws, frame-independence of zero coordinate acceleration, and the group of frame changes). Here $a$ denotes the spatial translation of the Example; $α$ denotes acceleration.

[L4]

Coordinate velocity, acceleration, spatial velocity vector and dimensions (Coordinate velocity and acceleration of a worldline in an inertial frame, and the spatial velocity and acceleration vectors, Dimensions and SI unit conventions of the non-relativistic classical mechanics framework).

Verification

Proof technique: direct; expand both adapted charts in the standard basis and check the displayed relations on the explicit data.

1.1L1algebra

The data of the Example satisfy [L1]: $τ$ is linear and surjective (its value is the first coordinate), $K = {0} \times R^{3}$ has dimension three, the standard inner product on $K$ is symmetric and positive definite, the standard orientation of $R^{3}$ orients $K$ , and $A = R^{4}$ is an affine space over itself.

1.2L2algebra

The constructed frame $F^{'}$ is inertial in the sense of [L2]: $τ (u^{'}) = 1$ because $u^{'} = (1, - \frac{1}{2}, 0, 0)$ , and the basis $(e_{1}^{'}, e_{2}^{'}, e_{3}^{'}) = (e_{1}, e_{2}, e_{3})$ is $g$ -orthonormal and positively oriented; hence $F^{'}$ is an adapted chart with adapted coordinates $(t^{'}, x^{'})$ .

1.3L3algebra

The primed coordinates of the event $p = t u + \sum_{j} x^{j} e_{j}$ are obtained by expanding $p = o^{'} + t^{'} u^{'} + \sum_{j} x^{' j} e_{j}^{'}$ : comparing components gives $t^{'} = t + 2$ and $x^{'} = (x^{1} + \frac{1}{2} t, x^{2} + 3, x^{3}) = R x + v t + a$ , so the two frames differ by the transformation of [L3] with the displayed parameters $(b, a, v, R)$ .

1.4givenL1L4algebra

The prescribed worldline $γ$ is of class $C^{\infty}$ and its $F$ -time coordinate is $τ (γ (s) - o) = s$ , so the parameter condition holds; its coordinate curve is $x (s)$ with coordinate velocity $w = (\frac{1}{4}, 0, 0)$ and coordinate acceleration $α (s) : = x^{''} (s) = 0$ .

2.1step 1.3step 1.4L3L4algebra

The primed description of the motion is $η (t^{'}) = x (t^{'} - 2) + v (t^{'} - 2) + a = (\frac{3}{4} t^{'} - \frac{1}{2}, 5, 0)$ ; hence $η^{'} = (\frac{3}{4}, 0, 0) = R w + v$ and $η^{''} (t^{'}) = (0, 0, 0) = R α (t^{'} - b)$ , so the velocity and acceleration laws of [L3] hold on this motion, and the vanishing of the coordinate acceleration is frame-independent for it.

3.1step 1.3step 2.1algebra

As a cross-check, at $t = 2$ the $F$ -coordinates are $(\frac{3}{2}, 2, 0)$ and the $F^{'}$ -coordinates of the same event are $η (4) = (\frac{5}{2}, 5, 0)$ , which equals $x (2) + 2 v + a$ by the transformation of step 1.3.

4.1step 2.1L4algebra∎

Finally, the spatial velocity vectors confirm the same laws: in $F$ one has $\underline{v} = γ^{'} (s) - u = \frac{1}{4} e_{1}$ , and in $F^{'}$ one has ${\underline{v}}^{'} = γ^{'} (s) - u^{'} = \frac{1}{4} e_{1} + \frac{1}{2} e_{1} = \frac{3}{4} e_{1}$ , whose primed-basis coordinates $(\frac{3}{4}, 0, 0)$ equal the coordinate velocity $η^{'}$ of step 2.1; the example thus verifies the transformation law and the velocity and acceleration laws on explicit data. It does not identify the displayed uniform motion with the motion of an unforced particle in any dynamical sense, which requires the force postulates of a later page.

A worked Galilean boost: the same uniform motion in two inertial frames

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources