LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passverified 2026-10-15 (gpt-6-luna, gpt-6.1-sol, and delegated Codex review/repair agents; see completed run evidence)

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.

Exact flat centroid translation and disk

Statement

Let $(A, V, η, C^{+})$ be an oriented, time-oriented affine Minkowski space, with signature $(- + + +)$ , and fix $c > 0$ . Let $p$ be any future timelike vector and define $M : = \sqrt{- η (p, p)} / c > 0$ . Choose an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ of Inertial frames and inertial charts of the affine Minkowski model with $e_{0} = p / (M c)$ , so its ordered orthonormal basis is future and positively oriented and $p$ has components $(M c, 0)$ in this frame. Its positive-definite rest space is $e_{0}^{⊥} = span (e_{1}, e_{2}, e_{3})$ ; use $(e_{1}, e_{2}, e_{3})$ for spatial components and the induced right-handed symbol $ϵ_{i j k}$ . Let $S^{a b} = - S^{b a}$ satisfy the momentum supplementary condition $S^{a b} p_{b} = 0$ , and set $s_{*}^{k} : = \frac{1}{2} ϵ_{k i j} S^{i j}$ in this oriented orthonormal rest-space basis. Every future unit observer has the components $n = γ (e_{0} + \sum_{i = 1}^{3} \frac{v^{i}}{c} e_{i}), γ = (1 - ∣ v ∣^{2} / c^{2})^{- 1 / 2}, ∣ v ∣ < c,$ by Norms of four-velocity and four-acceleration, and the observer rest-space decomposition. For every such observer, define $δ^{a} : = \frac{S^{a b} n_{b}}{p \cdot n}, S^{' a b} : = S^{a b} - (δ^{a} p^{b} - δ^{b} p^{a}) .$ Then $p \cdot n \neq 0$ , $δ \cdot p = δ \cdot n = 0$ , and $S^{' a b} n_{b} = 0$ . Let $z \in A$ be the representative event. For $u, v \in V$ , define $(u \land v)^{a b} : = u^{a} v^{b} - u^{b} v^{a}$ . If the representative point changes by $z \mapsto z + δ$ , the total angular momentum about the frame origin $o$ , $J_{o} : = (z - o) \land p + S,$ is unchanged by this stipulated spin-shift rule. In the rest space, $δ = \frac{s_{*} \times v}{M c^{2}},$ If $s_{*} \neq 0$ , the shifts of all future timelike observers fill the open disk in $s_{*}^{⊥}$ of radius $∣ s_{*} ∣ / (M c)$ ; the boundary is a supremum and is not attained. If $s_{*} = 0$ , only the zero shift occurs. This is an exact affine-flat algebraic result.

Facts & Assumptions

Given: The oriented, time-oriented affine Minkowski model, a fixed $c > 0$ , a future timelike momentum $p = (M c, 0)$ with $M > 0$ , an antisymmetric $S$ , the stated supplementary condition, and a future unit observer with $∣ v ∣ < c$ .

[A1]

The momentum supplementary condition $S^{a b} p_{b} = 0$ and the displayed spin-shift rule for the representative point are algebraic hypotheses of this flat model.

[F1]

Minkowski spacetime is an oriented time-oriented affine space with Lorentz form of signature $(- + + +)$ ; an inertial frame is a future, positively oriented orthonormal frame with its affine chart. Oriented time-oriented affine Minkowski space (the spacetime primitives); Inertial frames and inertial charts of the affine Minkowski model

[F2]

Relative to the inertial observer $e_{0}$ , a future unit observer has spatial velocity $v \in e_{0}^{⊥}$ , $∣ v ∣ < c$ , and components $γ (1, v / c)$ with $γ = (1 - ∣ v ∣^{2} / c^{2})^{- 1 / 2}$ ; $e_{0}^{⊥}$ is positive definite. Norms of four-velocity and four-acceleration, and the observer rest-space decomposition

[F3]

The spatial cross product is $(u \times v)_{i} = ϵ_{i j k} u_{j} v_{k}$ . The cross product in $R^{3}$

Proof

technique · direct

1.1givenA1F1F2algebra

Since $S^{a b} p_{b} = 0$ and $p = (M c, 0)$ , antisymmetry gives $S^{0 i} = 0$ . The observer decomposition [F2] gives $p \cdot n = - M c γ \neq 0$ , while $n_{a} n_{b} S^{a b} = 0$ and $p_{a} S^{a b} = 0$ give $δ \cdot n = δ \cdot p = 0$ . The definition $s_{*}^{k} = \frac{1}{2} ϵ_{k i j} S^{i j}$ inverts to $S^{i j} = ϵ_{i j k} s_{*}^{k}$ : contracting the right-hand side with $\frac{1}{2} ϵ_{ℓ i j}$ gives $s_{*}^{ℓ}$ by $\frac{1}{2} ϵ_{ℓ i j} ϵ_{i j k} = δ_{ℓ k}$ .

2.1givenA1step 1.1algebra

Contracting the spin-shift rule with $n_{b}$ yields $S^{' a b} n_{b} = S^{a b} n_{b} - δ^{a} (p \cdot n) + p^{a} (δ \cdot n) = 0,$ because $δ^{a} (p \cdot n) = S^{a b} n_{b}$ by definition and step 1.1 gives $δ \cdot n = 0$ . Also $(z + δ - o) \land p + S^{'} = (z - o) \land p + S$ , which proves the asserted invariance of $J_{o}$ .

2.2givenA1step 1.1F3algebra

In rest coordinates, $n_{j} = γ v_{j} / c$ , $p \cdot n = - M c γ$ , and step 1.1 gives $S^{i j} = ϵ_{i j k} s_{*}^{k}$ . Therefore $δ^{i} = \frac{ϵ_{i j k} s_{*}^{k} γ v_{j} / c}{- M c γ} = \frac{ϵ_{i j k} s_{*}^{j} v_{k}}{M c^{2}} = \frac{(s_{*} \times v)_{i}}{M c^{2}}, δ^{0} = 0.$ The second equality uses antisymmetry of $ϵ_{i j k}$ when interchanging $j, k$ .

3.1givenA1step 2.2F3algebra∎

Expanding the coordinate definition [F3] gives $∣ u \times v ∣^{2} = \sum_{i < j} (u_{i} v_{j} - u_{j} v_{i})^{2} = ∣ u ∣^{2} ∣ v ∣^{2} - (u \cdot v)^{2}$ and $u \times (v \times w) = v (u \cdot w) - w (u \cdot v)$ . Hence $∣ δ ∣ \leq ∣ s_{*} ∣ ∣ v ∣ / (M c^{2}) < ∣ s_{*} ∣ / (M c)$ for $s_{*} \neq 0$ . Conversely, for any $δ ⊥ s_{*}$ with $∣ δ ∣ < ∣ s_{*} ∣ / (M c)$ , choose $v = (M c^{2} / ∣ s_{*} ∣^{2}) (δ \times s_{*})$ . The expanded triple-product identity gives $s_{*} \times v = M c^{2} δ$ , and the norm identity gives $∣ v ∣ = M c^{2} ∣ δ ∣ / ∣ s_{*} ∣ < c$ . Thus every interior point occurs; equality in the radius would require $∣ v ∣ = c$ , excluded for a timelike observer. When $s_{*} = 0$ , the formula of step 2.2 gives only $δ = 0$ .

Remarks

The spin-shift rule is part of the algebraic hypotheses. This item does not assert a curved-spacetime translation law, a stress-integral theorem, or a material-body model.

Depends on

Dependency tree · 2 levels

Sources

L. Filipe Costa and José Natário, Center of mass, spin supplementary conditions, and the momentum of spinning particles, arXiv:1410.6443v2; published in Equations of Motion in Relativistic Gravity, Fundamental Theories of Physics 179 (Springer, 2015)