LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Transformation between adapted charts and its kinematic consequences

Statement

Let $(V, τ, g, A)$ be as in Affine time space with Euclidean simultaneous slices and adapted charts and let $(o, u, (e_{1}, e_{2}, e_{3}))$ and $(o^{'}, u^{'}, (e_{1}^{'}, e_{2}^{'}, e_{3}^{'}))$ be two adapted charts, with coordinate functions $(t, x)$ and $(t^{'}, x^{'})$ of Existence and uniqueness of adapted coordinates, and the affine structure of simultaneous slices.

There are $b \in R$ , $a, v \in R^{3}$ and a matrix $R \in O (3)$ such that for every $p \in A$

$t^{'} (p) = t (p) + b, x^{'} (p) = R x (p) + v t (p) + a .$

If $(e_{1}, e_{2}, e_{3})$ and $(e_{1}^{'}, e_{2}^{'}, e_{3}^{'})$ are both positively oriented for the fixed orientation of $K$ , then $R \in S O (3)$ (The orthogonal group $O (3)$ and the rotation group $S O (3)$ ).

Let $I \subseteq R$ be a nondegenerate interval and let $γ : I \to A$ be a map whose first-chart time coordinate satisfies $t (γ (s)) = s$ for all $s \in I$ . Write $x (s) : = x (γ (s))$ and $y (s) : = x^{'} (γ (s))$ . The regularity hypothesis below means that this coordinate function $x : I \to R^{3}$ is continuously differentiable (respectively, twice continuously differentiable); no additional smooth structure on $A$ is assumed. If $x$ is continuously differentiable then $y$ is continuously differentiable with

$y^{'} (s) = R x^{'} (s) + v (s \in I),$

and if $x$ is twice continuously differentiable then $y^{''} (s) = R x^{''} (s)$ for all $s \in I$ . Equivalently, in the differentiated variables of the two charts, $d x^{'} / d t^{'} = R d x / d t + v$ and $d^{2} x^{'} / d t^{' 2} = R d^{2} x / d t^{2}$ .

Consequently $x^{''} = 0$ on $I$ if and only if $y^{''} = 0$ on $I$ : the two charts agree on which time-parametrized curves have zero coordinate acceleration.

Facts & Assumptions

Given: Two adapted charts $(o, u, (e_{1}, e_{2}, e_{3}))$ and $(o^{'}, u^{'}, (e_{1}^{'}, e_{2}^{'}, e_{3}^{'}))$ of the data $(V, τ, g, A)$ , with coordinate functions $(t, x)$ and $(t^{'}, x^{'})$ ; for clauses 2 and 3 a map $γ : I \to A$ with $t (γ (s)) = s$ , and its first-chart spatial coordinate $x (s)$ of the stated regularity.

[L1]

Affine displacement identities: $p + (q - p) = q$ , $(q - p) + (r - q) = r - p$ , and displacements are additive over the action, as recorded in Affine time space with Euclidean simultaneous slices and adapted charts.

[L2]

$τ$ is linear with $τ (u) = τ (u^{'}) = 1$ and $K = \ker τ$ ; hence $τ (u - u^{'}) = 0$ , so $u - u^{'} \in K$ ; moreover $τ (o - o^{'}) = t^{'} (o) - t (o)$ is a constant (Affine time space with Euclidean simultaneous slices and adapted charts).

[L3]

Adapted coordinates are unique, and for each slice $A_{t}$ the coordinate vector of $p - o - t u \in K$ in the basis $(e_{1}, e_{2}, e_{3})$ is $x (p)$ ; likewise for the primed chart (Existence and uniqueness of adapted coordinates, and the affine structure of simultaneous slices).

[L4]

Both ordered bases are $g$ -orthonormal and positively oriented; if $M$ is the change-of-basis matrix defined by $e_{j} = \sum_{k} M_{k j} e_{k}^{'}$ , then $M^{T} M = I_{3}$ , and $\det M > 0$ because the two bases lie in the same orientation class. Determinant multiplicativity and invariance under transpose give $(\det M)^{2} = \det (M^{T} M) = 1$ ; positivity and uniqueness of the positive square root give $\det M = 1$ . Hence $M \in O (3)$ , and $M \in S O (3)$ under the orientation hypothesis of clause 1 (Orientation of a finite-dimensional real vector space, Orthogonal vectors and subspaces, orthogonal and orthonormal sets, and orthonormal bases, The orthogonal group $O (3)$ and the rotation group $S O (3)$ , For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ , For same-sized finite square matrices over a commutative ring, $\det (A B) = \det (A) \det (B)$ , Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[L5]

A fixed matrix applied to a $C^{1}$ vector-valued curve, plus an affine function of the parameter, is $C^{1}$ and differentiates componentwise; if the curve is $C^{2}$ , differentiating again gives the same fixed matrix times its second derivative (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

Proof

technique · direct

1.1L1L2L3algebra

By the slice formula of [L3] applied at $p$ and at $o$ , $t^{'} (p) - t (p) = τ (p - o^{'}) - τ (p - o) = τ (o - o^{'})$ , which does not depend on $p$ ; put $b : = τ (o - o^{'})$ . This proves the first display of clause 1.

2.1step 1.1L1L2L3algebra

Let $k : = p - o - t u = \sum_{i} x_{i} (p) e_{i} \in K$ and $k^{'} : = p - o^{'} - t^{'} u^{'} = \sum_{i} x_{i}^{'} (p) e_{i}^{'} \in K$ . Subtracting the second expansion from the first and using [L1], $k^{'} = k + (o - o^{'}) + (t - t^{'}) u + t^{'} (u - u^{'})$ . Here $(o - o^{'}) + (t - t^{'}) u \in K$ because its $τ$ -value is $b - b = 0$ by step 1.1 and [L2], and $t^{'} (u - u^{'}) \in K$ by [L2]; hence the displayed equality is an identity in $K$ .

3.1step 1.1step 2.1L1L3L4algebra

Let $c \in R^{3}$ be the coordinate vector in the unprimed basis of the constant vector $(o - o^{'}) + (t - t^{'}) u \in K$ , and let $d \in R^{3}$ be the coordinate vector of $u - u^{'} \in K$ ; by step 2.1 and [L3], the coordinate vector of $k^{'}$ in the unprimed basis is $x (p) + c + t^{'} (p) d$ . Since the coordinate vector of $k^{'}$ in the primed basis is $x^{'} (p)$ and changes of coordinates are given by [L4], $x^{'} (p) = M (x (p) + c + t^{'} (p) d) = M x (p) + (M d) t^{'} (p) + M c$ . Using $t^{'} = t + b$ from step 1.1 and setting $R : = M$ , $v : = M d$ , $a : = M c + b v$ , this reads $x^{'} (p) = R x (p) + v t (p) + a$ , the second display of clause 1.

4.1step 3.1L4algebra

By [L4], $M^{T} M = I_{3}$ , so $R = M \in O (3)$ ; and if both bases are positively oriented then $\det M > 0$ , which with $\det M = \pm 1$ gives $\det M = 1$ and $R \in S O (3)$ . This completes clause 1.

4.2step 3.1L5algebra

For the map $γ$ with $t (γ (s)) = s$ , clause 1 gives $y (s) = x^{'} (γ (s)) = R x (s) + v s + a$ . By [L5], this coordinate function is $C^{1}$ with $y^{'} (s) = R x^{'} (s) + v$ , and if $x$ is $C^{2}$ it satisfies $y^{''} (s) = R x^{''} (s)$ . Since $t^{'} (γ (s)) = s + b$ , one has $d t^{'} / d s = 1$ , giving the equivalent differentiated-coordinate formulas. This proves clause 2.

5.1step 4.2L4algebra∎

If $x^{''} = 0$ on the interval then $y^{''} = R x^{''} = 0$ by step 4.2; conversely if $y^{''} = 0$ then $0 = R^{T} y^{''} = R^{T} R x^{''} = x^{''}$ because $R^{T} R = I_{3}$ by [L4]. This proves clause 3.

Transformation between adapted charts and its kinematic consequences

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources