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.

Uniform Christoffel-symbol bounds for stationary weak-field data

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} φ : U \to R$ (Stationary weak-field data: the diagonal ansatz, its bounds, stationarity and the Einstein-family condition), let $c > 0$ , and let $ε_{*}$ and $C_{1}$ be the threshold and constant of Stationarity, timelikeness and uniform inverse-metric bounds for stationary weak-field data. Then there is $C_{2} < \infty$ , depending only on $C$ , $L$ and the dimension, such that for every $0 < ε \leq ε_{*}$ the Christoffel symbols $Γ^{a}_{b c}$ of the metric-selected connection of $g (ε)$ in the inertial chart satisfy the following bounds at every spacetime point $p \in Ω$ with $π (p) \in K$ :

$∣ Γ^{i}_{00} - \frac{\partial_{i} Φ}{c^{2}} ∣ \leq \frac{C_{2} ε^{2}}{L}, ∣ Γ^{i}_{0 j} ∣ \leq \frac{C_{2} ε^{3 / 2}}{L}, ∣ Γ^{i}_{j k} ∣ \leq \frac{C_{2} ε}{L},$

$∣ Γ^{0}_{00} ∣ \leq \frac{C_{2} ε^{5 / 2}}{L}, ∣ Γ^{0}_{0 j} ∣ \leq \frac{C_{2} ε}{L}, ∣ Γ^{0}_{j k} ∣ \leq \frac{C_{2} ε^{3 / 2}}{L},$

for all $i, j, k \in {1, 2, 3}$ , with the maximum over the free spatial indices.

Facts & Assumptions

Given: Stationary weak-field data and $0 < ε \leq ε_{*}$ , with $Φ = ε c^{2} φ$ .

Write $\tilde{Φ} : = Φ \circ π$ and $\tilde{φ} : = φ \circ π$ for their stationary lifts to $Ω$ ; then $\partial_{0} \tilde{Φ} = \partial_{0} \tilde{φ} = 0$ .

[L1]

$Γ^{a}_{b c} = \frac{1}{2} \sum_{d} g^{a d} (\partial_{b} g_{c d} + \partial_{c} g_{b d} - \partial_{d} g_{b c})$ in the chart, and the components of the inverse metric satisfy $∣ \partial^{α} g^{a b} (ε) ∣ \leq C_{1} / L^{∣ α ∣}$ on the spacetime portion over $K$ for $∣ α ∣ \leq 2$ , together with the sharp expansion $g^{a b} (ε) = η^{a b} - η^{a c} E_{c d} (ε) η^{d b} + R^{a b} (ε)$ with $E = g (ε) - η$ and $∣ R^{a b} (ε) ∣ \leq C_{1} ε^{2}$ , which in particular gives $∣ g^{a b} (ε) - η^{a b} ∣ \leq C_{1} ε$ , $∣ g^{00} + 1 ∣ \leq C_{1} ε$ , and $∣ g^{0 i} (ε) ∣ \leq C_{1} ε^{3 / 2}$ (Christoffel symbols of an affine connection, Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields, Metric compatibility, torsion freedom and the metric-selected connection class, Stationarity, timelikeness and uniform inverse-metric bounds for stationary weak-field data).

[L2]

The metric coefficients are pullbacks from $U$ : $g_{00} = - (1 + 2 ε φ) + r_{00}$ , $g_{i j} = (1 - 2 ε φ) δ_{i j} + r_{i j}$ , $g_{0 i} = r_{0 i}$ ; for spatial $i$ , $∣ \partial_{i} r_{00} ∣ + ∣ \partial_{i} r_{j k} ∣ \leq C ε^{2} / L$ , $∣ \partial_{i} r_{0 j} ∣ \leq C ε^{3 / 2} / L$ , and $∣ \partial_{i} φ ∣ \leq C / L$ on $K$ , while all time derivatives of the pulled-back components vanish (Stationary weak-field data: the diagonal ansatz, its bounds, stationarity and the Einstein-family condition clause (a)).

[L3]

Derivatives of sums and products obey the usual rules and component fields are smooth (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).

Proof

technique · direct; insert the explicit components and their uniform derivative bounds into the Christoffel formula, using stationarity to cancel all time derivatives

1.1L2algebra

(Derivative bounds of the metric components.) By [L2], for spatial $i$ one has $\partial_{i} \tilde{Φ} = ε c^{2} \partial_{i} φ$ and $∣ \partial_{i} φ ∣ \leq C / L$ , so $∣ \partial_{i} g_{00} ∣ \leq 2 ε C / L + C ε^{2} / L \leq C^{'} ε / L$ , $∣ \partial_{i} g_{j k} ∣ \leq C^{'} ε / L$ and $∣ \partial_{i} g_{0 j} ∣ \leq C ε^{3 / 2} / L$ . All time derivatives of the metric components are zero by stationarity.

2.1step 1.1L1L2L3algebra

(The component with two lower zeros.) By [L1] and stationarity [L2], $Γ^{i}_{00} = \frac{1}{2} g^{i a} (2 \partial_{0} g_{a 0} - \partial_{a} g_{00}) = - \frac{1}{2} g^{i a} \partial_{a} g_{00} = \frac{1}{2} g^{i a} (2 \partial_{a} \tilde{Φ} / c^{2} - \partial_{a} r_{00})$ , since $\partial_{a} g_{00} = - 2 ε \partial_{a} \tilde{φ} + \partial_{a} r_{00} = - 2 \partial_{a} \tilde{Φ} / c^{2} + \partial_{a} r_{00}$ . Write $g^{i a} = η^{i a} + (g^{i a} - η^{i a})$ and use $η^{i a} \partial_{a} \tilde{Φ} = \partial_{i} Φ$ , because $i \neq 0$ and the only nonzero entries of $η^{i a}$ with $i \neq 0$ are the spatial $δ^{i a}$ : the first term gives $\partial_{i} Φ / c^{2}$ , while $∣ (g^{i a} - η^{i a}) \partial_{a} \tilde{Φ} / c^{2} ∣ \leq C_{1} ε \cdot C ε / L$ by [L1] and [L2] and $∣ \frac{1}{2} g^{i a} \partial_{a} r_{00} ∣ \leq \frac{1}{2} C^{'} C ε^{2} / L$ ; hence $∣ Γ^{i}_{00} - \partial_{i} Φ / c^{2} ∣ \leq C_{2} ε^{2} / L$ .

2.2step 1.1L1L2L3algebra

(The remaining components.) Again by [L1] and stationarity, $Γ^{i}_{0 j} = \frac{1}{2} g^{i a} (\partial_{j} g_{a 0} - \partial_{a} g_{0 j})$ . Split the sum into $a = 0$ and spatial $a = k$ : the $a = 0$ term is $\frac{1}{2} g^{i 0} \partial_{j} g_{00}$ , bounded by $C^{'} ε^{5 / 2} / L$ using [L1], [L2] and step 1.1; each spatial term $\frac{1}{2} g^{i k} (\partial_{j} r_{k 0} - \partial_{k} r_{0 j})$ is bounded by $C^{'} ε^{3 / 2} / L$ using [L1] and [L2]. These bounds are uniform in $p \in K$ and $0 < ε \leq ε_{*}$ , and their finite sum gives $∣ Γ^{i}_{0 j} ∣ \leq C_{2} ε^{3 / 2} / L$ . Next, $Γ^{i}_{j k} = \frac{1}{2} g^{i a} (\partial_{j} g_{a k} + \partial_{k} g_{a j} - \partial_{a} g_{j k})$ ; splitting off the explicit $φ$ -terms leaves $\frac{1}{2} g^{i a} (- 2 ε) (δ_{a k} \partial_{j} \tilde{φ} + δ_{a j} \partial_{k} \tilde{φ} - δ_{j k} \partial_{a} \tilde{φ})$ , whose absolute value is at most $C^{'} ε / L$ by [L1] and [L2], while the $r$ -terms contribute at most $C^{'} ε^{2} / L$ ; hence $∣ Γ^{i}_{j k} ∣ \leq C_{2} ε / L$ . For the components with upper index $0$ , use the sharp inverse expansion of [L1], $g^{0 a} = η^{0 a} - η^{0 c} E_{c d} η^{d a} + R^{0 a}$ , with $∣ R^{0 a} ∣ \leq C_{1} ε^{2}$ : the inverse bounds in [L1] give $∣ g^{00} + 1 ∣ \leq C_{1} ε$ , $∣ g^{0 i} ∣ \leq C_{1} ε^{3 / 2}$ and $∣ g^{00} ∣ \leq C_{1}$ . For $Γ^{0}_{00} = \frac{1}{2} g^{0 a} (2 \partial_{0} g_{a 0} - \partial_{a} g_{00}) = - \frac{1}{2} g^{0 a} \partial_{a} g_{00}$ the $a = 0$ term vanishes by stationarity and the $a = i$ term contributes at most $\frac{1}{2} C^{'} ε^{3 / 2} \cdot C^{'} ε / L \leq C_{2} ε^{5 / 2} / L$ . For $Γ^{0}_{0 j} = \frac{1}{2} g^{0 a} (\partial_{j} g_{a 0} - \partial_{a} g_{0 j})$ the $a = 0$ term is $\frac{1}{2} g^{00} \partial_{j} g_{00}$ with $∣ g^{00} ∣ \leq C_{1}$ and $∣ \partial_{j} g_{00} ∣ \leq C^{'} ε / L$ , and the $a = i$ term is $\frac{1}{2} g^{0 i} (\partial_{j} r_{i 0} - \partial_{i} r_{0 j})$ of size at most $C^{'} ε^{3 / 2} \cdot C^{'} ε^{3 / 2} / L \leq C^{'} ε^{3} / L$ ; hence $∣ Γ^{0}_{0 j} ∣ \leq C_{2} ε / L$ . Finally $Γ^{0}_{j k} = \frac{1}{2} g^{0 a} (\partial_{j} g_{a k} + \partial_{k} g_{a j} - \partial_{a} g_{j k})$ : the $a = 0$ term is $\frac{1}{2} g^{00} (\partial_{j} r_{0 k} + \partial_{k} r_{0 j})$ of size at most $C_{1} C ε^{3 / 2} / L \leq C^{'} ε^{3 / 2} / L$ , and the $a = i$ term is at most $C^{'} ε^{3 / 2} \cdot C^{'} ε / L \leq C^{'} ε^{5 / 2} / L$ ; hence $∣ Γ^{0}_{j k} ∣ \leq C_{2} ε^{3 / 2} / L$ .

3.1step 2.1step 2.2given∎

(Conclusion.) Steps 2.1 and 2.2 give every displayed bound with a constant depending only on $C$ , $L$ and the dimension; the constants of the weaker displayed inequalities were enlarged.

Remarks

Here $O (ε^{a} / L^{b})$ means a bound in absolute value by $C ε^{a} / L^{b}$ uniform in $p \in K$ and $0 < ε \leq ε_{*}$ ; the constant may depend on the fixed data bounds, $L$ and the dimension.

Sources of the upper-bound orders. The leading contributions are explicit: $Γ^{0}_{00}$ is controlled by $- \frac{1}{2} g^{0 i} \partial_{i} g_{00} = O (ε^{5 / 2} / L)$ and $Γ^{0}_{j k}$ by $\frac{1}{2} g^{00} (\partial_{j} r_{0 k} + \partial_{k} r_{0 j}) = O (ε^{3 / 2} / L)$ , while the leading term in $Γ^{0}_{0 j}$ is $\frac{1}{2} g^{00} \partial_{j} g_{00} = ε \partial_{j} φ + O (ε^{2} / L)$ . These products explain the uniform upper-bound orders used by the weak-field applications; a component may be smaller or vanish for particular data, and no lower bound or saturation is claimed.
Stationarity is used. The cancellation of the time-derivative terms in steps 2.1 and 2.2 is exactly where $\partial_{0} g = 0$ enters; without it the leading term of $Γ^{i}_{00}$ would contain contributions from $\partial_{0} g_{0 i}$ .

Uniform Christoffel-symbol bounds for stationary weak-field data

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources