TheoremStatement: 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 of tensor, covector, derivative and current components under affine Lorentz maps

Statement

Let $(A, V, η, C^{+})$ be the affine Minkowski space, let $x$ and $x^{'}$ be inertial charts whose transition is the affine map $x^{'} (p) = Λ x (p) + b$ with linear part $Λ$ (a proper orthochronous Lorentz matrix by Inertial charts are related by proper orthochronous affine Lorentz maps, and every such map is a chart transition), and let $Ω \subseteq A$ be an open subset. Fix $ℓ \in N \cup {\infty}$ and $r, s \in N$ . Let $J : Ω \to V$ , $k : Ω \to V^{*}$ and $T : Ω \to T^{r, s} (V)$ be a $C^{ℓ}$ vector field, a $C^{ℓ}$ covector field and a $C^{ℓ}$ type- $(r, s)$ tensor field on $Ω$ in the sense of C^k tensor fields on affine Minkowski space and their inertial components, with components $J^{a}$ , $k_{a}$ and $T^{a_{1} \dots a_{r}}_{b_{1} \dots b_{s}}$ in the chart $x$ , and primed components in the chart $x^{'}$ . Use indices $a, b \in {0, 1, 2, 3}$ and $i \in {1, 2, 3}$ , summing every repeated upper/lower index. All component identities compare the same event $p$ ; as coordinate functions their arguments are $u = x (p)$ and $u' = x' (p) = Λ u + b$ . Then:

(i) $J^{' a} = Λ^{a}_{b} J^{b}$ : a contravariant index gains the factor $Λ^{a}_{b}$ , that is, components transform by multiplication with the transition matrix;

(ii) $k_{a}^{'} = (Λ^{- 1})^{b}_{a} k_{b}$ : a covariant index gains the factor $(Λ^{- 1})^{b}_{a}$ . If $θ (p) = k_{a} x^{a} (p) + θ_{0}$ is an affine scalar function with constant covector $k$ and constant $θ_{0}$ , then $θ (p) = k_{a}^{'} x^{' a} (p) + θ_{0}^{'}$ with $k^{'}$ as above and $θ_{0}^{'} : = θ_{0} - k_{a}^{'} b^{a}$ , so the phase function is invariant when the constant term is transformed together with the covector;

(iii) $T^{' a_{1} \dots a_{r}}_{b_{1} \dots b_{s}} = Λ^{a_{1}}_{c_{1}} \dots Λ^{a_{r}}_{c_{r}} (Λ^{- 1})^{d_{1}}_{b_{1}} \dots (Λ^{- 1})^{d_{s}}_{b_{s}} T^{c_{1} \dots c_{r}}_{d_{1} \dots d_{s}}$ : every contravariant index gains a factor $Λ$ and every covariant index a factor $Λ^{- 1}$ , and the law is consistent with the multilinear evaluation of $T (p)$ after substituting the transformed basis. Every contraction of one contravariant with one covariant index is invariant, and the metric components satisfy $η_{a b}^{'} = η_{a b}$ ;

(iv) the coordinate partial-derivative operators satisfy $\partial_{a}^{'} = (Λ^{- 1})^{b}_{a} \partial_{b}$ when applied to scalar functions at points where their coordinate representations are totally differentiable. Consequently, at every event where the component functions of $J$ are totally differentiable, the divergence is invariant, $\partial_{a}^{'} J^{' a} = \partial_{a} J^{a}$ . These total differentials exist at every event if $ℓ \geq 1$ ; for $ℓ = 0$ this clause applies only at events where the specified components are totally differentiable, and does not assert covariance from the existence of separate partial derivatives alone. For a $C^{1}$ type- $(2, 0)$ field $T$ one has $\partial_{a}^{'} T^{' a b} = Λ^{b}_{c} \partial_{a} T^{a c}$ ;

(v) alternating covariant tensor fields transform by the covariant law on each slot; the oriented volume form of the model satisfies $ϵ_{a b c d}^{'} = ϵ_{a b c d}$ , since $\det Λ = + 1$ , whereas a general Lorentz matrix with $\det = - 1$ changes its sign;

(vi) let $J$ be a $C^{1}$ vector field with components $(J^{0}, J^{1}, J^{2}, J^{3})$ in an inertial chart, and write the spatial block as $J_{c o v} : = (J^{1}, J^{2}, J^{3})$ and denote by $\partial_{i}$ the spatial partial derivatives in the chart. Then the continuity equation $\partial_{a} J^{a} = 0$ is equivalent to $\partial_{0} J^{0} + \sum_{i} \partial_{i} J^{i} = 0$ , and under the passive boost with parameter $β$ ( $Λ = B (β)$ , $Λ^{- 1} = B (- β)$ ) the components transform as $J^{' 0} = γ (J^{0} - β \cdot J_{c o v})$ and $J_{c o v}^{'} = J_{c o v} + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot J_{c o v}) β - γ β J^{0}$ ;

(vii) if $U$ is a $C^{1}$ future timelike vector field and $ρ_{0}$ a $C^{1}$ scalar field, then $J : = ρ_{0} U$ is a $C^{1}$ vector field and its first component is $J^{0} = ρ_{0} U^{0}$ . Future timelikeness gives $U^{0} > 0$ in every inertial chart, so one may define the normalized chart direction $u : = U / U^{0}$ and the coordinate density $ρ : = J^{0}$ . Then $u^{0} = 1$ , $u^{i} = U^{i} / U^{0}$ , $ρ = ρ_{0} U^{0}$ , and $J = ρ u$ pointwise. The coordinate density $ρ$ and scalar multiplier $ρ_{0}$ are different objects: $ρ = ρ_{0}$ if and only if $ρ_{0} (U^{0} - 1) = 0$ ; at points where $ρ_{0} \neq 0$ equality holds exactly when $U^{0} = 1$ . The vector $u$ is a normalized chart direction; it is not assumed to have unit or four-velocity normalization. In an $x^{0} = c t$ convention the associated spatial coordinate velocity, if interpreted as such, has components $c u^{i}$ ; physical current/density identification requires its own model premise.

Interpretation boundary. The identification of a physical charge-current with a vector field, and of $ρ$ with a measured charge density, is a model premise of the electromagnetic framework; this item is a statement about the transformation of components of specified fields and does not by itself assert that any physical current transforms as a vector.

Facts & Assumptions

Given: The regularity index $ℓ \in N \cup {\infty}$ and ranks $r, s \in N$ , the affine Minkowski space with inertial charts $x, x^{'}$ related by $x^{'} (p) = Λ x (p) + b$ , the open set $Ω \subseteq A$ , and the fields $J, k, T$ of the Statement with their components in both charts.

[L1]

The transition of two inertial charts is affine with linear part $Λ = M^{- 1}$ , where $M$ is the matrix of the proper orthochronous linear Lorentz map $L$ with $L e_{a} = e_{a}^{'}$ and $Λ$ is the matrix of $L^{- 1}$ ; the linear parts of transitions are exactly the proper orthochronous Lorentz matrices and their inverses (Inertial charts are related by proper orthochronous affine Lorentz maps, and every such map is a chart transition).

[L2]

A linear Lorentz map is a linear isomorphism preserving $η$ ; its matrix in an orthonormal basis satisfies the metric condition; it is proper when its determinant is $+ 1$ and orthochronous when it maps $C^{+}$ onto $C^{+}$ ; the affine Lorentz maps form a group (Linear and affine Lorentz maps, and the Lorentz group, Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups).

[L3]

A $C^{ℓ}$ type- $(r, s)$ tensor field on $Ω$ assigns to $p \in Ω$ a multilinear $T (p) : (V^{*})^{r} \times V^{s} \to R$ , with components $T^{a_{1} \dots a_{r}}_{b_{1} \dots b_{s}} (p) = T (p) (e^{* a_{1}}, \dots, e_{b_{1}}, \dots)$ in a frame, and regularity is chart-independent (C^k tensor fields on affine Minkowski space and their inertial components, A type $(r, s)$ tensor on a finite-dimensional vector space).

[L4]

A type- $(1, 0)$ tensor is a vector and a type- $(0, 1)$ tensor a covector $V \to R$ ; a basis $(e_{a})$ of $V$ has a dual basis $(e^{* a})$ of $V^{*}$ with $e^{* a} (e_{b}) = δ_{b}^{a}$ (A type $(r, s)$ tensor on a finite-dimensional vector space, Linear functionals and the algebraic dual $V^{*} = L (V, F)$ ).

[L5]

The contraction of the first contravariant slot with the first covariant slot of a type- $(r, s)$ tensor with $r, s \geq 1$ is the type- $(r - 1, s - 1)$ tensor $ctr (T) (α_{2}, \dots, v_{2}, \dots) = \sum_{i} T (e^{i}, α_{2}, \dots, e_{i}, \dots)$ , and the value is independent of the basis used (The contraction of a mixed tensor, Contraction is independent of the basis formula).

[L6]

An alternating $k$ -linear map is a $k$ -linear map vanishing whenever two arguments coincide (Alternating $k$ -linear maps); the oriented volume form of the model is $ϵ (v_{0}, \dots, v_{3}) = \det ([v_{j}^{a}])$ in an inertial frame, an alternating $4$ -linear form with $ϵ_{0123} = + 1$ (The oriented volume form epsilon and the permutation symbols of an inertial frame).

[L7]

For a proper linear Lorentz map $L$ the oriented volume form satisfies $ϵ (L v_{0}, \dots, L v_{3}) = ϵ (v_{0}, \dots, v_{3})$ , and for $\det L = - 1$ the two sides differ by the sign $- 1$ (Lorentz maps are isomorphisms of determinant ±1 that preserve causal character and permute the cones; the Lorentz sets are groups).

[L8]

At $β = 0$ the boost is the identity; the quotient expressions in clause (vi) and the proof are used only for nonzero $β$ , with their spatial correction interpreted as zero at $β = 0$ . The passive boost with parameter $β$ has the coordinate action and matrix displayed in The passive Lorentz boost with parameter beta, with inverse $B (- β)$ , and $γ = (1 - ∣ β ∣^{2})^{- 1 / 2}$ (The passive boost is a proper orthochronous Lorentz map with inverse B(-beta)).

[L9]

In an inertial chart, $x (p) = E^{- 1} (p - o)$ with $E$ the coordinate isomorphism and $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)_{a b}$ (Inertial frames and inertial charts of the affine Minkowski model). For the conditional coordinate-velocity interpretation in clause (vii), fix a real constant $c > 0$ and define the reparametrized coordinate $t : = x^{0} / c$ . This is a mathematical rescaling; no SI unit or physical-clock identification is assumed.

[L10]

The affine model $(A, V, η, C^{+})$ has interval $I (p, q) = η (q - p, q - p)$ and its events and displacements carry no additional structure (Oriented time-oriented affine Minkowski space (the spacetime primitives)).

[L11]

In an $η$ -orthonormal basis the timelike set has components described by $T_{+} = {x : x^{0} > ∣ x_{v e c} ∣}$ and $T_{-} = {x : x^{0} < - ∣ x_{v e c} ∣}$ , in particular every future timelike vector has strictly positive time coordinate (The timelike set has exactly two convex components, described in orthonormal coordinates).

[L12]

Partial derivatives satisfy the chain rule: if $g$ is totally differentiable at $a$ and $f$ at $g (a)$ , then $D (f \circ g) (a) = D f (g (a)) \circ D g (a)$ (The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set); sums, scalar multiples and products of differentiable functions obey the algebra of derivatives (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$ ), and matrix multiplication has the usual index rule (Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, Linear map between vector spaces over the same field).

[L13]

Under $T_{p} A = V$ , $\partial_{a} ∣_{p}$ denotes the coordinate tangent vector corresponding to $e_{a}$ ; $d x^{a} ∣_{p}$ denotes its dual covector, characterized by $d x^{a} (\partial_{b}) = δ_{b}^{a}$ . This is the canonical tangent identification of The tangent space of the affine Minkowski model at any event is canonically V and the finite dual-basis construction of The dual family $(b^{*})_{b \in B}$ associated to a Hamel basis $B$ , defined by $b^{*} (c) = δ_{b c}$ , not an additional regularity assumption.

Proof

technique · direct

1.1L1L2L12algebraL10

Write the transition as $x^{' a} = Λ^{a}_{c} x^{c} + b^{a}$ with $Λ$ invertible, $\det Λ = + 1$ and $Λ$ orthochronous by [L1] and [L2]; the inverse relation is $x^{c} = (Λ^{- 1})^{c}_{a} (x^{' a} - b^{a})$ . At a point where the scalar coordinate representation is totally differentiable, the affine coordinate maps are differentiable, so the total chain rule [L12] gives $\partial_{c} = \frac{\partial x^{' a}}{\partial x^{c}} \partial_{a}^{'} = Λ^{a}_{c} \partial_{a}^{'}$ and $\partial_{a}^{'} = \frac{\partial x^{c}}{\partial x^{' a}} \partial_{c} = (Λ^{- 1})^{c}_{a} \partial_{c}$ , and the two matrices are inverse: $Λ^{a}_{c} (Λ^{- 1})^{c}_{d} = δ_{d}^{a}$ and $(Λ^{- 1})^{c}_{a} Λ^{a}_{d} = δ_{d}^{c}$ by [L12].

1.2L9L11L12algebra

For (vii), let $U$ be $C^{1}$ future timelike and $ρ_{0}$ a $C^{1}$ scalar; then $J = ρ_{0} U$ has components $J^{a} = ρ_{0} U^{a}$ and is $C^{1}$ by the product rule of [L12]. In an inertial chart the future timelike vectors are the coordinate set $C^{+} = {x : x^{0} > ∣ x_{v e c} ∣}$ by [L11] and [L9], so $U^{0} > 0$ and $u : = U / U^{0}$ is well defined with $u^{0} = 1$ and $u^{i} = U^{i} / U^{0}$ ; moreover $ρ : = J^{0} = ρ_{0} U^{0}$ and $J = ρ_{0} U = ρ_{0} U^{0} (U / U^{0}) = ρ u$ . Since $ρ - ρ_{0} = ρ_{0} (U^{0} - 1)$ , one has $ρ = ρ_{0}$ exactly when $ρ_{0} (U^{0} - 1) = 0$ , and when $ρ_{0} \neq 0$ this is equivalent to $U^{0} = 1$ . The vector $u$ has first component $1$ but is not asserted to satisfy any unit or four-velocity normalization; with the convention $x^{0} = c t$ of [L9], a curve whose coordinate tangent is proportional to $U$ has $d x^{i} / d t = c U^{i} / U^{0} = c u^{i}$ . No identification of $J$ with a physical current is made: the Interpretation boundary of the Statement records that this requires a model premise. This proves (vii).

2.1L3L4L13step 1.1algebra

For the vector field, [L3] and [L4] write $J = J^{c} \partial_{c}$ in the chart $x$ and $J = J^{' a} \partial_{a}^{'}$ in the chart $x^{'}$ ; substituting $\partial_{c} = Λ^{a}_{c} \partial_{a}^{'}$ from step 1.1 gives $J = J^{c} Λ^{a}_{c} \partial_{a}^{'}$ , and comparing coefficients in the basis $(\partial_{a}^{'})$ of the tangent space gives $J^{' a} = Λ^{a}_{c} J^{c}$ ; this proves (i).

2.2L4L12L13step 1.1algebra

For the covector field, write $k = k_{b} d x^{b}$ and $k = k_{a}^{'} d x^{' a}$ ; since $x^{c} = (Λ^{- 1})^{c}_{a} (x^{' a} - b^{a})$ , the chain rule [L12] gives $d x^{c} = (Λ^{- 1})^{c}_{a} d x^{' a}$ , so $k = k_{b} (Λ^{- 1})^{b}_{a} d x^{' a}$ and comparing coefficients gives $k_{a}^{'} = (Λ^{- 1})^{b}_{a} k_{b}$ . For the phase function, substitute the inverse relation: $k_{a} x^{a} + θ_{0} = k_{a} (Λ^{- 1})^{a}_{c} (x^{' c} - b^{c}) + θ_{0} = k_{c}^{'} x^{' c} + θ_{0} - k_{c}^{'} b^{c}$ , where the last step uses $k_{c}^{'} = k_{a} (Λ^{- 1})^{a}_{c}$ ; hence $θ = k_{a}^{'} x^{' a} + θ_{0}^{'}$ with $θ_{0}^{'} = θ_{0} - k_{a}^{'} b^{a}$ , and the phase function has the same value at every event in both charts. This proves (ii).

2.3L1L2L3L4L5step 1.1algebra

For the tensor law, [L1] gives $e_{a}^{'} = L e_{a}$ with $L$ proper orthochronous and matrix $M$ satisfying $e_{a}^{'} = M^{b}_{a} e_{b}$ with $M = Λ^{- 1}$ ; consequently the dual bases satisfy $e^{' * a} = Λ^{a}_{b} e^{* b}$ (both sides pair with $e_{c}^{'} = \sum_{b} (Λ^{- 1})^{b}_{c} e_{b}$ to give $δ_{c}^{a}$ by [L4] and the inverse relations of step 1.1). By the component definition of [L3] and multilinearity of $T (p)$ , $T^{' a_{1} \dots a_{r}}_{b_{1} \dots b_{s}} = T (p) (e^{' * a_{1}}, \dots, e_{b_{1}}^{'}, \dots) = Λ^{a_{1}}_{c_{1}} \dots (Λ^{- 1})^{d_{1}}_{b_{1}} \dots T^{c_{1} \dots c_{r}}_{d_{1} \dots d_{s}}$ , which is the displayed law. Contracting the first contravariant with the first covariant index in the transformed components gives $Λ^{a}_{c} (Λ^{- 1})^{d}_{a} \dots = δ^{d}_{c} \dots$ , which is the contraction of the untransformed components; the remaining free indices retain their respective transformation factors, yielding precisely the component law of the same type- $(r - 1, s - 1)$ tensor $ctr (T)$ . Thus contraction is invariant as an intrinsic operation, as [L5] states; a fully contracted scalar has the same numerical value in both charts. For the metric, its components are $η_{a b} = η (e_{a}, e_{b})$ in any frame, and by [L2] and [L1] $η_{a b}^{'} = η (e_{a}^{'}, e_{b}^{'}) = η (L e_{a}, L e_{b}) = η (e_{a}, e_{b}) = η_{a b} = diag (- 1, 1, 1, 1)_{a b}$ in every inertial frame. This proves (iii).

3.1L12step 1.1step 2.3algebra

At an event where all coordinate components of $J$ are totally differentiable, linear combinations and affine precomposition preserve total differentiability by [L12]; this is automatic for $ℓ \geq 1$ and is the additional pointwise hypothesis for $ℓ = 0$ . For the derivative law on a totally differentiable scalar, step 1.1 gives $\partial_{a}^{'} = (Λ^{- 1})^{b}_{a} \partial_{b}$ . For the divergence, (i) gives $J^{' a} = Λ^{a}_{c} J^{c}$ , so $\partial_{a}^{'} J^{' a} = (Λ^{- 1})^{b}_{a} \partial_{b} (Λ^{a}_{c} J^{c}) = δ^{b}_{c} \partial_{b} J^{c} = \partial_{a} J^{a}$ , using the inverse relations of step 1.1 and the index rule of [L12]. For a $C^{1}$ type- $(2, 0)$ field all components are totally differentiable; (iii) gives $T^{' a b} = Λ^{a}_{c} Λ^{b}_{d} T^{c d}$ , hence $\partial_{a}^{'} T^{' a b} = (Λ^{- 1})^{e}_{a} \partial_{e} (Λ^{a}_{c} Λ^{b}_{d} T^{c d}) = δ^{e}_{c} Λ^{b}_{d} \partial_{e} T^{c d} = Λ^{b}_{d} \partial_{a} T^{a d}$ . This proves (iv).

3.2L1L6L7step 2.3algebra

An alternating covariant tensor field is a covariant tensor field by [L6], so the covariant law of (iii) applies on each slot and no further structure is involved. For the oriented volume form, its components in the two frames are $ϵ_{a b c d} = ϵ (e_{a}, e_{b}, e_{c}, e_{d})$ and $ϵ_{a b c d}^{'} = ϵ (e_{a}^{'}, e_{b}^{'}, e_{c}^{'}, e_{d}^{'})$ by [L6]; since $e_{a}^{'} = L e_{a}$ with $L$ proper by [L1], [L7] gives $ϵ_{a b c d}^{'} = ϵ (L e_{a}, L e_{b}, L e_{c}, L e_{d}) = \det (L) ϵ (e_{a}, e_{b}, e_{c}, e_{d}) = ϵ_{a b c d}$ , while for $\det L = - 1$ the same computation gives the opposite sign. This proves (v).

4.1L8step 2.1step 3.1algebra

For $β = 0$ , [L8] gives $J^{'} = J$ directly; the spatial correction in (vi) is zero by that convention. For nonzero $β$ , clause (vi) is the special case of (i) and (iv) for the passive boost: the continuity equation is the component expansion $\partial_{a} J^{a} = \partial_{0} J^{0} + \sum_{i} \partial_{i} J^{i}$ , and substituting $Λ = B (β)$ , $Λ^{- 1} = B (- β)$ into $J^{' a} = Λ^{a}_{b} J^{b}$ and reading the matrix entries of [L8] gives $J^{' 0} = γ (J^{0} - β \cdot J_{c o v})$ and $J_{c o v}^{'} = J_{c o v} + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot J_{c o v}) β - γ β J^{0}$ .

5.1step 2.1step 2.2step 2.3step 3.1step 3.2step 4.1step 1.2∎

Clause (i) is step 2.1, clause (ii) is step 2.2, clause (iii) is step 2.3, clause (iv) is step 3.1, clause (v) is step 3.2, clause (vi) is step 4.1 and clause (vii) is step 1.2; the Interpretation boundary is a restriction on the reading of the components and is not used as a premise anywhere. This proves every clause of the statement.

Transformation of tensor, covector, derivative and current components under affine Lorentz maps

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources