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

Coordinate-time acceleration of weak-field geodesics: the Newtonian leading term with uniform error

Statement

Let $(Ω, K, L, C, ε_{0}, φ, r)$ be stationary weak-field data with spatial base $U = π (Ω)$ , compact $K \subseteq U$ and spatial potential $Φ = ε c^{2} φ$ (Stationary weak-field data: the diagonal ansatz, its bounds, stationarity and the Einstein-family condition), let $c > 0$ , let $ε_{*}$ and $C_{2}$ be the threshold and constant of Uniform Christoffel-symbol bounds for stationary weak-field data, let $0 < ε \leq ε_{*}$ , and let $Γ^{a}_{b c}$ be the Christoffel symbols of $g (ε)$ in the inertial chart.

(a) Reparametrization identity. Let $γ : S \to Ω$ be a geodesic of $g (ε)$ in an affine parameter $s$ on an interval $S$ (Geodesic of an affine connection), suppose that $t (s) : = x^{0} (γ (s)) / c$ is $C^{2}$ with $d t / d s \neq 0$ on $S$ and has image an interval $I$ , and write $x (t)$ for the spatial coordinates of $γ$ and $z (t) : = (c t, x (t))$ for its full chart-coordinate curve. Set $u^{a} : = d z^{a} / d t = (c, \dot{x})$ ; the geodesic equation holds in the chart (Coordinate geodesic equation). Then for every $t \in I$ ,

$\frac{d^{2} x^{i}}{d t^{2}} = - Γ^{i}_{b c} u^{b} u^{c} + \frac{u^{i}}{c} Γ^{0}_{b c} u^{b} u^{c} .$

(b) Newtonian leading term. Suppose in addition that $γ (t) = (c t, x (t)) \in Ω$ , $x (t) \in K$ and $∣ \dot{x} (t) ∣ \leq C \sqrt{ε} c$ for every $t \in I$ . Then there is $C_{3} < \infty$ , depending only on $C$ , $L$ and the dimension, such that for every $t \in I$ and $i = 1, 2, 3$ ,

$∣ \frac{d^{2} x^{i}}{d t^{2}} + \partial_{i} Φ (x (t)) ∣ \leq \frac{C_{3} c^{2} ε^{2}}{L} .$

Facts & Assumptions

Given: Stationary weak-field data with spatial base $U = π (Ω)$ , $0 < ε \leq ε_{*}$ , a geodesic $γ$ reparametrized by $t = x^{0} / c$ , with $γ (t) = (c t, x (t)) \in Ω$ , spatial path $x (t) \in K \subseteq U$ and $∣ \dot{x} ∣ \leq C \sqrt{ε} c$ .

[L1]

At every spacetime point with spatial coordinate in $K$ and for the given $ε$ , the Christoffel symbols of $g (ε)$ satisfy $∣ Γ^{i}_{00} - \partial_{i} Φ / c^{2} ∣ \leq C_{2} ε^{2} / L$ , $∣ Γ^{i}_{0 j} ∣ \leq C_{2} ε^{3 / 2} / L$ , $∣ Γ^{i}_{j k} ∣ \leq C_{2} ε / L$ , $∣ Γ^{0}_{00} ∣ \leq C_{2} ε^{5 / 2} / L$ , $∣ Γ^{0}_{0 j} ∣ \leq C_{2} ε / L$ and $∣ Γ^{0}_{j k} ∣ \leq C_{2} ε^{3 / 2} / L$ (Uniform Christoffel-symbol bounds for stationary weak-field data, with supplies Stationary weak-field data: the diagonal ansatz, its bounds, stationarity and the Einstein-family condition, Stationarity, timelikeness and uniform inverse-metric bounds for stationary weak-field data, Metric compatibility, torsion freedom and the metric-selected connection class, Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields and Christoffel symbols of an affine connection).

[L2]

In a chart, a curve is a geodesic in an affine parameter $s$ if and only if $\frac{d^{2} z^{a}}{d s^{2}} + \sum_{b, c} Γ^{a}_{b c} (z) \frac{d z^{b}}{d s} \frac{d z^{c}}{d s} = 0$ , where $z = x \circ γ$ ; the chain rule and the quotient rule for $C^{2}$ curves apply to the change of parameter (Coordinate geodesic equation, 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$ , $C^{r}$ and smooth maps between smooth manifolds, The flat model spacetime: the Minkowski metric on R^4 and its inertial chart).

Proof

technique · direct; reparametrize the chart geodesic equation by the coordinate time, then insert the uniform Christoffel bounds

1.1L2givenalgebra

(Reparametrization identity.) Write $v^{a} : = d z^{a} / d s$ for the affine velocity of the geodesic and $u^{a} : = d z^{a} / d t$ for its coordinate-time velocity, so that $v^{0} = c d t / d s \neq 0$ and $u^{a} = c v^{a} / v^{0}$ ; in particular $u^{0} = c$ , so $u = (c, \dot{x})$ . The geodesic equation of [L2] reads $d v^{a} / d s = - Γ^{a}_{b c} v^{b} v^{c}$ . Since $v^{a} = (v^{0} / c) u^{a}$ , substituting $v^{b} v^{c} = (v^{0} / c)^{2} u^{b} u^{c}$ and using the chain rule $\frac{d}{d t} = \frac{c}{v^{0}} \frac{d}{d s}$ gives $\frac{d^{2} x^{i}}{d t^{2}} = \frac{c}{v^{0}} \frac{d}{d s} (\frac{c v^{i}}{v^{0}}) = \frac{c^{2}}{(v^{0})^{2}} \frac{d v^{i}}{d s} - \frac{c^{2} v^{i}}{(v^{0})^{3}} \frac{d v^{0}}{d s} = - Γ^{i}_{b c} u^{b} u^{c} + \frac{u^{i}}{c} Γ^{0}_{b c} u^{b} u^{c},$ which is (a).

1.2givenalgebra

(Uniform smallness of the velocity data.) The hypothesis $∣ \dot{x} ∣ \leq C \sqrt{ε} c$ and $u^{0} = c$ give $∣ u^{a} ∣ \leq \max (c, C \sqrt{ε} c) \leq C_{4} c$ for a constant $C_{4}$ depending only on $C$ , since $ε \leq ε_{*} \leq 1$ by the definition of the threshold.

2.1step 1.1step 1.2L1algebra

(Insertion of the bounds.) Insert the components of the identity of step 1.1 and the estimates of [L1], using step 1.2 to bound the velocity factors: $- c^{2} Γ^{i}_{00} = - \partial_{i} Φ + O (c^{2} ε^{2} / L), ∣ 2 c Γ^{i}_{0 j} {\dot{x}}^{j} ∣ \leq 2 c \cdot \frac{C_{2} ε^{3 / 2}}{L} \cdot C \sqrt{ε} c = \frac{C^{'} c^{2} ε^{2}}{L},$ $∣ Γ^{i}_{j k} {\dot{x}}^{j} {\dot{x}}^{k} ∣ \leq \frac{C_{2} ε}{L} \cdot C^{2} ε c^{2} = \frac{C^{''} c^{2} ε^{2}}{L},$ and each of the three terms containing the factor ${\dot{x}}^{i} / c$ is bounded by $C^{'''} c^{2} ε^{2} / L$ : for the $Γ^{0}_{00}$ term, $∣ {\dot{x}}^{i} ∣ c ∣ Γ^{0}_{00} ∣ \leq C \sqrt{ε} c \cdot c \cdot C_{2} ε^{5 / 2} / L = C^{'''} c^{2} ε^{3} / L \leq C^{'''} c^{2} ε^{2} / L$ ; for the $Γ^{0}_{0 j}$ term, $∣ 2 {\dot{x}}^{i} Γ^{0}_{0 j} {\dot{x}}^{j} ∣ \leq 2 C \sqrt{ε} c \cdot C_{2} ε / L \cdot C \sqrt{ε} c$ ; and for the $Γ^{0}_{j k}$ term, $∣ {\dot{x}}^{i} Γ^{0}_{j k} {\dot{x}}^{j} {\dot{x}}^{k} ∣ / c \leq C \sqrt{ε} \cdot C_{2} ε^{3 / 2} / L \cdot C^{2} ε c^{2}$ . Collecting all terms and renaming the constants gives (b).

3.1step 1.1step 2.1given∎

(Conclusion.) Step 1.1 proves (a) and step 2.1 proves (b), with constants depending only on $C$ , $L$ and the dimension.

Remarks

Coordinate time, not proper time. The parameter $t = x^{0} / c$ is the chart time; the conversion from proper time to $t$ along the worldline is part of the reparametrization of step 1.1 and uses only $d t / d s \neq 0$ . No synchronization of distant clocks and no global time function is asserted.
Uniform in the family. The error term is uniform on $K$ and for the whole family, with constant depending only on $(C, L)$ ; this uniformity is what the trajectory-limit theorem on this page uses.
Scope. The estimate concerns the model's geodesics only: no claim is made that any physical body follows these geodesics, and the slow-motion and small-field conditions are hypotheses, not consequences.

Coordinate-time acceleration of weak-field geodesics: the Newtonian leading term with uniform error

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources