Physics 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.

Covariance, boosts and the two field invariants

Physical scope

Conditional statement on the smooth branch of the framework's Maxwell fields in one inertial chart: the exact passive-boost component formulas for $E, B$ along one spatial axis and in every vector direction (including the zero boost), invariance of $B^{2} - E^{2} / c^{2}$ and $E \cdot B$ under every proper orthochronous change of inertial description, the rotation and general-factorization laws, and form-invariance of the four Maxwell equations. Excluded: accelerating coordinates, curved spacetime, media, weak or singular fields, orientation-reversing changes, apparatus and any measurement or empirical claim.

Statement

Let $E, B$ be jointly $C^{k}$ fields of The electric and magnetic fields as fixed-time spatial vector fields on the laboratory region $U ≅ I \times Ω$ of an inertial chart $x$ of the framework (Laboratory geometry: a restricted inertial chart, its spatial slices and fixed-time fields), $k \geq 1$ , with the SI units of Framework-local SI units, the vacuum constants and the exact/measured status of their values, and let $F$ be the electromagnetic two-form of The electromagnetic two-form, its observer decomposition and the four-current with its fixed components $F_{0 i} = - E_{i} / c$ , $F_{i j} = ϵ_{i j k} B_{k}$ , $F^{0 i} = E_{i} / c$ , $F^{i j} = ϵ_{i j k} B_{k}$ . Let $0 \leq β < 1$ , $γ : = (1 - β^{2})^{- 1 / 2}$ , $v : = β c e_{1}$ , and let $Λ_{β}$ be the explicit boost of The explicit Lorentz boost preserves $η$ , has determinant $1$ and preserves the future cone with $Λ_{β}^{0}_{0} = Λ_{β}^{1}_{1} = γ$ , $Λ_{β}^{0}_{1} = Λ_{β}^{1}_{0} = - γ β$ , $Λ_{β}^{2}_{2} = Λ_{β}^{3}_{3} = 1$ and all other entries zero. Let $x^{'} = Λ_{β} x + b$ be the corresponding inertial chart, and for every event $p$ in the overlap of the two chart restrictions define the primed field components by reading the components of the same $F$ in $x^{'}$ through the dictionary of The electromagnetic two-form, its observer decomposition and the four-current, so that $F_{0 i}^{'} = - E_{i}^{'} / c$ , $F_{i j}^{'} = ϵ_{i j k} B_{k}^{'}$ at $p$ . Then:

(a) [Boosted fields] at every such $p$ , with $∥$ and $⊥$ the components along and orthogonal to $e_{1}$ in the spatial Euclidean structure of the chart, $E_{1}^{'} = E_{1}, B_{1}^{'} = B_{1}, E_{∥}^{'} = E_{∥}, B_{∥}^{'} = B_{∥}, E_{⊥}^{'} = γ (E + v \times B)_{⊥}, B_{⊥}^{'} = γ (B - v \times E / c^{2})_{⊥},$ equivalently, componentwise, $E_{2}^{'} = γ (E_{2} - β c B_{3})$ , $E_{3}^{'} = γ (E_{3} + β c B_{2})$ , $B_{2}^{'} = γ (B_{2} + β E_{3} / c)$ , $B_{3}^{'} = γ (B_{3} - β E_{2} / c)$ .

(a′) [Arbitrary boost direction] For a velocity vector $v \in R^{3}$ with $∣ v ∣ < c$ , use the actual vector boost $B (v / c)$ of The passive Lorentz boost with parameter beta, with $γ_{v} = (1 - ∣ v ∣^{2} / c^{2})^{- 1 / 2}$ . If $v \neq 0$ , decompose the fields along $\hat{v} = v / ∣ v ∣$ and its orthogonal complement. Then $E_{∥}^{'} = E_{∥}$ , $B_{∥}^{'} = B_{∥}$ , $E_{⊥}^{'} = γ_{v} (E + v \times B)_{⊥}$ and $B_{⊥}^{'} = γ_{v} (B - v \times E / c^{2})_{⊥}$ . Equivalently, for every $v$ , including $v = 0$ , $E^{'} = γ_{v} (E + v \times B) - \frac{γ_{v}^{2}}{γ_{v} + 1} \frac{v (v \cdot E)}{c^{2}}, B^{'} = γ_{v} (B - v \times E / c^{2}) - \frac{γ_{v}^{2}}{γ_{v} + 1} \frac{v (v \cdot B)}{c^{2}} .$ At $v = 0$ these are the identity and no preferred parallel direction is assigned.

(b) [Invariants] at every such $p$ , $∣ B^{'} ∣^{2} - \frac{∣ E^{'} ∣^{2}}{c^{2}} = ∣ B ∣^{2} - \frac{∣ E ∣^{2}}{c^{2}}, E^{'} \cdot B^{'} = E \cdot B;$ equivalently the scalar fields $I_{1} : = \frac{1}{2} F_{a b} F^{a b} = ∣ B ∣^{2} - ∣ E ∣^{2} / c^{2}$ and $I_{2} : = F_{a b} (* F)^{a b} = 4 E \cdot B / c$ of The electromagnetic two-form, its observer decomposition and the four-current (b) take the same values whether computed from the components in $x$ or in $x^{'}$ .

(c) [General proper orthochronous changes] for any proper orthochronous Lorentz matrix $Λ$ with chart $x^{'} = Λ x + b$ , the primed components of $F$ are given by the component law of Transformation of tensor, covector, derivative and current components under affine Lorentz maps (iii), $F^{' a b} = Λ^{a}_{c} Λ^{b}_{d} F^{c d}$ ; in particular, if $Λ = \hat{R}$ is the extension of a spatial rotation $R$ of the frame (Spatial rotations of an inertial frame), then $E^{'} = R E$ and $B^{'} = R B$ , and by the unique factorization $Λ = B (- β) \hat{R}$ of The proper orthochronous Lorentz group: boosts, rotations, unique factorization and invariants (iii) every proper orthochronous change acts first by $(E, B) \mapsto (R E, R B)$ and then by the arbitrary-direction boost law (a′) with velocity $- c β$ , where $β$ is the vector parameter of that factorization. The axis-only law (a) is not substituted for a general vector boost.

(d) [Form invariance of the Maxwell branch] if $(E, B, ρ, J)$ satisfy the smooth branch of The microscopic vacuum Maxwell equations: smooth and weak branches in $x$ on the overlap, and $(ρ^{'}, J^{'})$ are the components of the same four-current in $x^{'}$ , then $(E^{'}, B^{'}, ρ^{'}, J^{'})$ satisfy the same four equations in $x^{'}$ , by Tensor Maxwell equations equal the four laboratory Maxwell equations.

(e) [Scope] All clauses are pointwise on the overlap $U \cap U^{'}$ of the two chart restrictions, are conditional on the adopted postulates, and concern the smooth classical flat branch; no accelerating coordinates, curved spacetime, material medium, apparatus or empirical claim is involved; the transformation is exact algebra, and the primed component functions are $C^{k}$ wherever the overlap is open. The invariants clause uses only the proper orthochronous changes of description adopted in Adopted inertial covariance of the model equations; orientation-reversing changes are outside the framework's field conventions (The electric and magnetic fields as fixed-time spatial vector fields).

Facts & Assumptions

Given: The inertial chart $x$ of the framework's laboratory region with the fields $E, B$ (jointly $C^{k}$ , $k \geq 1$ ) and the continuous sources $(ρ, J)$ , and the SI units of Framework-local SI units, the vacuum constants and the exact/measured status of their values; the electromagnetic two-form $F$ with the dictionary, invariants and conventions of [F1]; the axis boost $Λ_{β}$ of [F2] with $0 \leq β < 1$ and its chart $x^{'} = Λ_{β} x + b$ ; a velocity vector $v \in R^{3}$ with $∣ v ∣ < c$ and the vector boost $B (v / c)$ of [F2]; a general proper orthochronous Lorentz matrix $Λ$ with chart $x^{'} = Λ x + b$ ; and the postulates [F4] and [F9]. Every primed component is read through the dictionary [F1].

[F1]

In the chart $x$ the electromagnetic two-form has components $F_{00} = 0$ , $F_{0 i} = - E_{i} / c$ , $F_{i j} = ϵ_{i j k} B_{k}$ , $F_{a b} = - F_{b a}$ and $F^{0 i} = E_{i} / c$ , $F^{i 0} = - E_{i} / c$ , $F^{i j} = ϵ_{i j k} B_{k}$ , where $η = diag (- 1, 1, 1, 1)$ and $ϵ_{i j k} = + 1$ for even, $- 1$ for odd permutations of $(1, 2, 3)$ and $0$ for repeated indices; its Hodge dual is $(* F)_{a b} = \frac{1}{2} ε_{a b}^{c d} F_{c d}$ and its scalar contractions are $I_{1} : = \frac{1}{2} F_{a b} F^{a b} = ∣ B ∣^{2} - ∣ E ∣^{2} / c^{2}$ and $I_{2} : = F_{a b} (* F)^{a b} = 4 E \cdot B / c$ , with $∣ \cdot ∣$ and $\cdot$ the spatial Euclidean structure of the frame (The electromagnetic two-form, its observer decomposition and the four-current (a), (b), Hodge decomposition of an alternating two-form for an observer, invariants and the optional field identification (a), (c)). The fields carry V m $^{- 1}$ and T, $E$ is a polar and $B$ an axial vector relative to the orientation of the spatial basis, only orientation-preserving changes of inertial description are adopted, and no value of a field at a point of singular source support is asserted (The electric and magnetic fields as fixed-time spatial vector fields (a)-(c), Framework-local SI units, the vacuum constants and the exact/measured status of their values (b)). The four-current is $j^{0} = c ρ$ , $j^{i} = J^{i}$ (Charge parameter, frame charge and current densities, volume charge and flux, and the four-current (c)).

[F2]

For $0 \leq β < 1$ and $γ = (1 - β^{2})^{- 1 / 2}$ the map $Λ_{β}$ with matrix $Λ_{β}^{0}_{0} = Λ_{β}^{1}_{1} = γ$ , $Λ_{β}^{0}_{1} = Λ_{β}^{1}_{0} = - γ β$ , $Λ_{β}^{2}_{2} = Λ_{β}^{3}_{3} = 1$ and all other entries zero is a proper orthochronous Lorentz map with $\det Λ_{β} = 1$ and $Λ_{β}^{- 1} = Λ_{- β}$ (The explicit Lorentz boost preserves $η$ , has determinant $1$ and preserves the future cone (a)-(d)). For $β \in R^{3}$ with $∣ β ∣ < 1$ and $γ (β) = (1 - ∣ β ∣^{2})^{- 1 / 2}$ , the vector boost $B (β)$ has matrix $B^{0}_{0} = γ (β)$ , $B^{0}_{i} = B^{i}_{0} = - γ (β) β_{i}$ , $B^{i}_{j} = δ^{i}_{j} + \frac{γ (β) - 1}{∣ β ∣^{2}} β_{i} β_{j}$ for $β \neq 0$ , and $B (0) = {id}_{V}$ ; it is a proper orthochronous Lorentz map with $B (β)^{- 1} = B (- β)$ , and for $β \neq 0$ one has $\frac{γ (β) - 1}{∣ β ∣^{2}} = \frac{γ (β)^{2}}{γ (β) + 1}$ (The passive Lorentz boost with parameter beta, The proper orthochronous Lorentz group: boosts, rotations, unique factorization and invariants (i)).

[F3]

For a second inertial chart $x^{'} = Λ x + b$ with $Λ$ proper orthochronous, the components of the same tensor and vector fields satisfy $F^{' a b} = Λ^{a}_{c} Λ^{b}_{d} F^{c d}$ , $F_{a b}^{'} = (Λ^{- 1})^{c}_{a} (Λ^{- 1})^{d}_{b} F_{c d}$ and $j^{' a} = Λ^{a}_{b} j^{b}$ , and every contraction of one contravariant with one covariant index is invariant (Transformation of tensor, covector, derivative and current components under affine Lorentz maps (i), (iii)).

[F4]

A change of inertial description is an affine map $x^{'} = Λ x + b$ whose linear part $Λ$ is a proper orthochronous Lorentz matrix ( $η$ -preserving, $\det = + 1$ , $C^{+}$ -preserving), and such a $Λ$ is invertible (Adopted inertial covariance of the model equations (ii)). Every vector boost $B (β)$ with $∣ β ∣ < 1$ and every spatial rotation of the frame belongs to $S O^{+} (V, η)$ , and every $L \in S O^{+} (V, η)$ has a unique factorization $L = B (- β) \hat{R}$ with $∣ β ∣ < 1$ and $\hat{R}$ the extension of a spatial rotation of the frame, where $β = u_{v e c} / u^{0}$ for $u = L e_{0}$ (The proper orthochronous Lorentz group: boosts, rotations, unique factorization and invariants (i)-(iii)).

[F5]

A spatial rotation $R$ of the frame fixes $e_{0}$ , preserves the spatial three-space $S$ , satisfies $δ (R w, R z) = δ (w, z)$ on $S$ , and its restriction has determinant $+ 1$ in the ordered basis $(e_{1}, e_{2}, e_{3})$ ; under the identification of $S$ with $R^{3}$ by that basis, the maps of these conditions are exactly those with block matrix $diag (1, A)$ where $A^{T} A = I_{3}$ and $\det A = + 1$ , so the columns of $A$ are an orthonormal family of $R^{3}$ (Spatial rotations of an inertial frame).

[F6]

For coordinate columns in $R^{3}$ the cross product is $u \times v = (u_{2} v_{3} - u_{3} v_{2}, u_{3} v_{1} - u_{1} v_{3}, u_{1} v_{2} - u_{2} v_{1})$ (The cross product in $R^{3}$ ); it is bilinear and alternating, $u \times v$ is orthogonal to $u$ and $v$ , and $⟨ u \times v, w ⟩ = \det [u v w]$ , where the bracket denotes the $3 \times 3$ matrix with these columns (The cross product is bilinear, alternating, and orthogonal to both factors); moreover $∥ u \times v ∥_{2}^{2} = ∥ u ∥_{2}^{2} ∥ v ∥_{2}^{2} - ⟨ u, v ⟩^{2}$ (The squared cross-product norm is the Gram determinant of two vectors). The Euclidean inner product is bilinear, symmetric and positive definite, so $⟨ z, z ⟩ = 0$ implies $z = 0$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[F7]

For a real $n \times n$ matrix $A$ one has $\det A = \sum_{σ \in S_{n}} sgn (σ) \prod_{i < n} A^{σ (i)}_{i}$ (sum over columns $i$ ); permuting the columns by a permutation $π$ multiplies the determinant by $sgn (π)$ , so a determinant with two equal columns vanishes and $\det I_{n} = 1$ (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix); $\det (A^{T}) = \det A$ (For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ ); $A$ is invertible if and only if $\det A \neq 0$ (A finite square real matrix is invertible if and only if its determinant is nonzero); and the determinant of a linear operator is the determinant of its coordinate matrix (The determinant of an endomorphism of a finite-dimensional vector space: its matrix determinant in an ordered basis in positive dimension, and $1$ on the zero space).

[F8]

Tensor Maxwell equations equal the four laboratory Maxwell equations: under that theorem's hypotheses, stated for the framework's chart $x$ , the four smooth-branch Maxwell equations hold on the laboratory region if and only if the two tensor systems $(T M 1)$ $\partial_{μ} F^{μ ν} = - μ_{0} j^{ν}$ and $(T M 2)$ $\partial_{λ} F_{μ ν} + \partial_{μ} F_{ν λ} + \partial_{ν} F_{λ μ} = 0$ hold there; and for a second inertial chart $x^{'} = Λ x + b$ with proper orthochronous $Λ$ , $(T M 1)$ holds in $x$ if and only if it holds in $x^{'}$ with $j^{'}$ , and $(T M 2)$ holds in $x$ if and only if it holds in $x^{'}$ ; consequently the four smooth-branch equations are form-invariant, the primed fields satisfying the primed equations with the primed sources (clauses (a), (b)).

[F9]

The smooth branch of the vacuum Maxwell postulate: for jointly $C^{1}$ fields with the additional derivatives required by each equation existing and continuous, and continuous sources, $div E = ρ / ε_{0}$ , $div B = 0$ , $curl E = - \partial_{t} B$ and $curl B = μ_{0} J + c^{- 2} \partial_{t} E$ (The microscopic vacuum Maxwell equations: smooth and weak branches (a)).

Proof

technique · direct component computation in the fixed dictionary, the explicit conjugation of the vector boost by a rotation, and the constant component law

1.1givenF1F2F3F6algebra

(Clause (a): the axis boost components) For a spatial vector $W$ write $W_{∥} : = (W \cdot e_{1}) e_{1}$ and $W_{⊥} : = W - W_{∥}$ . By [F2] and F3, $F^{' a b} = Λ_{β}^{a}_{c} Λ_{β}^{b}_{d} F^{c d}$ on the overlap; substituting the nonzero entries of [F2] and the components of [F1] gives $F^{' 01} = Λ^{0}_{0} Λ^{1}_{1} F^{01} + Λ^{0}_{1} Λ^{1}_{0} F^{10} = γ^{2} (1 - β^{2}) F^{01} = F^{01}$ , $F^{' 02} = Λ^{0}_{0} Λ^{2}_{2} F^{02} + Λ^{0}_{1} Λ^{2}_{2} F^{12} = γ (E_{2} / c - β B_{3})$ , $F^{' 03} = γ (E_{3} / c + β B_{2})$ , $F^{' 12} = Λ^{1}_{0} Λ^{2}_{2} F^{02} + Λ^{1}_{1} Λ^{2}_{2} F^{12} = γ (B_{3} - β E_{2} / c)$ , $F^{' 13} = - γ (B_{2} + β E_{3} / c)$ and $F^{' 23} = F^{23} = B_{1}$ , because $F^{00} = F^{11} = 0$ , $F^{10} = - E_{1} / c$ , $F^{02} = E_{2} / c$ , $F^{03} = E_{3} / c$ , $F^{12} = B_{3}$ , $F^{13} = - B_{2}$ and $F^{23} = B_{1}$ by [F1]. Reading the dictionary [F1] in the primed chart, $E_{i}^{'} = c F^{' 0 i}$ and $F^{' i j} = ϵ_{i j k} B_{k}^{'}$ , gives $E_{1}^{'} = E_{1}$ , $E_{2}^{'} = γ (E_{2} - β c B_{3})$ , $E_{3}^{'} = γ (E_{3} + β c B_{2})$ , $B_{1}^{'} = B_{1}$ , $B_{2}^{'} = γ (B_{2} + β E_{3} / c)$ and $B_{3}^{'} = γ (B_{3} - β E_{2} / c)$ . Since $v = β c e_{1}$ , the coordinate formulas of [F6] give $v \times B = β c (0, - B_{3}, B_{2})$ and $v \times E = β c (0, - E_{3}, E_{2})$ ; hence $(E + v \times B)_{⊥} = (0, E_{2} - β c B_{3}, E_{3} + β c B_{2})$ and $(B - v \times E / c^{2})_{⊥} = (0, B_{2} + β E_{3} / c, B_{3} - β E_{2} / c)$ , so the transverse formulas and the unchanged parallel components read $E_{∥}^{'} = E_{∥}$ , $B_{∥}^{'} = B_{∥}$ , $E_{⊥}^{'} = γ (E + v \times B)_{⊥}$ and $B_{⊥}^{'} = γ (B - v \times E / c^{2})_{⊥}$ , as claimed.

1.2givenF1F3F5F6F7algebra

(Clause (c), rotation case; the orientation identity) Let $A \in M_{3} (R)$ satisfy $A^{T} A = I_{3}$ and $\det A = + 1$ , and let $Λ = diag (1, A)$ ; then the components $F^{' a b} = Λ^{a}_{c} Λ^{b}_{d} F^{c d}$ of [F3] satisfy $E^{'} = A E$ and $B^{'} = A B$ . First $F^{' 0 i} = A^{i}_{j} F^{0 j}$ , so $E_{i}^{'} = c F^{' 0 i} = A^{i}_{j} E_{j}$ . For the magnetic block, the dictionary gives $B_{q}^{'} = \frac{1}{2} ϵ_{q i j} F^{' i j}$ , since inserting $F^{' i j} = ϵ_{i j p} B_{p}^{'}$ yields $\frac{1}{2} ϵ_{q i j} ϵ_{i j p} B_{p}^{'} = δ_{q p} B_{p}^{'}$ by the elementary contraction $ϵ_{q i j} ϵ_{i j p} = 2 δ_{q p}$ (direct enumeration of the two contributing index pairs). Hence $B_{q}^{'} = \frac{1}{2} ϵ_{q i j} A^{i}_{k} A^{j}_{l} ϵ_{k l m} B_{m}$ , and the matrix $A$ satisfies the cofactor identity $ϵ_{q i j} A^{i}_{k} A^{j}_{l} = A^{q}_{m} ϵ_{m k l}$ for all $q, k, l$ : the determinant of the matrix with columns $(c_{m}, c_{k}, c_{l})$ of $A$ equals $ϵ_{m k l} \det A = ϵ_{m k l}$ by column alternation [F7], and it also equals $\sum_{n, i, j} ϵ_{n i j} A^{n}_{m} A^{i}_{k} A^{j}_{l}$ by the permutation expansion [F7]; multiplying that equality by $A^{q}_{m}$ and summing over $m$ turns the factor $A^{q}_{m} A^{n}_{m}$ into $(A A^{T})^{q n} = δ^{q n}$ and yields the identity, where $A A^{T} = I_{3}$ holds because $A^{T} A = I_{3}$ with $\det A = 1 \neq 0$ makes $A$ invertible with inverse $A^{T}$ [F7]. Then $B_{q}^{'} = \frac{1}{2} A^{q}_{m} ϵ_{m k l} ϵ_{k l p} B_{p} = A^{q}_{m} δ_{m p} B_{p} = A^{q}_{m} B_{m}$ by the elementary identity $ϵ_{m k l} ϵ_{k l p} = 2 δ_{m p}$ (direct enumeration), so $B^{'} = A B$ . If $A$ is the matrix in the basis $(e_{1}, e_{2}, e_{3})$ of a spatial rotation $R$ of the frame, then $A^{T} A = I_{3}$ and $\det A = + 1$ by [F5], and $E^{'} = R E$ , $B^{'} = R B$ , which is the rotation case of clause (c).

1.3givenF2F6F7choosealgebra

(Conjugation of the vector boost) Let $v \in R^{3}$ with $0 < ∣ v ∣ < c$ , put $u : = v / ∣ v ∣$ and $β : = ∣ v ∣ / c \in (0, 1)$ , so $v / c = β u$ . Among the standard basis vectors $e_{1}, e_{2}, e_{3}$ at most one is a multiple of $u$ (two independent vectors cannot both be nonzero multiples of one vector), so let $j \in {1, 2, 3}$ be the least index for which $e_{j}$ is not a multiple of $u$ ; set $\hat{a} : = (e_{j} - (e_{j} \cdot u) u) / ∥ e_{j} - (e_{j} \cdot u) u ∥_{2}$ , whose denominator is nonzero because $e_{j}$ is not a multiple of $u$ , and $b : = u \times \hat{a}$ . Then $(u, \hat{a}, b)$ is an orthonormal family, since $u \cdot \hat{a} = 0$ , $∥ u ∥_{2} = ∥ \hat{a} ∥_{2} = 1$ , $b$ is orthogonal to $u$ and $\hat{a}$ , and $∥ b ∥_{2}^{2} = ∥ u ∥_{2}^{2} ∥ \hat{a} ∥_{2}^{2} - (u \cdot \hat{a})^{2} = 1$ [F6]; it is positively oriented because $\det [u \hat{a} b] = ⟨ u \times \hat{a}, b ⟩ = ∥ b ∥_{2}^{2} = 1$ [F6]. Let $S$ be the matrix with columns $u, \hat{a}, b$ and $R : = S^{T}$ , so the rows of $R$ are $u, \hat{a}, b$ and $R u = e_{1}$ ; then $S^{T} S = I_{3}$ , $\det S = 1$ and, since $\det S = 1 \neq 0$ , $S$ is invertible with $S^{- 1} = S^{T}$ , so $S S^{T} = I_{3}$ , $R^{- 1} = R^{T}$ and $\det R = \det (S^{T}) = \det S = 1$ [F7]. The conjugation identity $\hat{R} B (v / c) {\hat{R}}^{- 1} = Λ_{β}$ , where $\hat{R} : = diag (1, R)$ , follows by direct substitution in the matrix of [F2]: for all $x \in V$ set $y : = \hat{R} x$ , so $y^{0} = x^{0}$ , $y_{v e c} = R x_{v e c}$ and $x_{v e c} = R^{T} y_{v e c}$ ; since $u \cdot x_{v e c} = u \cdot R^{T} y_{v e c} = (R u) \cdot y_{v e c} = y_{v e c}^{1}$ and $(v / c) \cdot x_{v e c} = β y_{v e c}^{1}$ , the formula of [F2] with parameter $β u$ gives $(\hat{R} B (v / c) x)^{0} = (B (v / c) x)^{0} = γ (x^{0} - β u \cdot x_{v e c}) = γ (y^{0} - β y_{v e c}^{1})$ and $(\hat{R} B (v / c) x)_{v e c} = R (R^{T} y_{v e c} + (γ - 1) y_{v e c}^{1} u - γ β y^{0} u) = y_{v e c} + (γ - 1) y_{v e c}^{1} e_{1} - γ β y^{0} e_{1}$ using $(R u) = e_{1}$ ; with $\hat{R} x = y$ this is exactly $Λ_{β} y$ by the matrix of [F2]. Hence $B (v / c) = {\hat{R}}^{T} Λ_{β} \hat{R}$ .

1.4givenF1F3F4algebra

(Regularity of the primed components) The overlap $V = U \cap U^{'}$ is open and carries both charts: $x (U) = {(c t, y) : t \in I, y \in Ω}$ and $x^{'} (U^{'})$ are open in $R^{4}$ , the affine map $x \mapsto Λ^{- 1} (x - b)$ carries $x^{'} (U^{'})$ bijectively onto $x (U^{'})$ , and $x$ carries $V$ onto the open set $x (U) \cap x (U^{'})$ because $x$ and $x^{'}$ are bijections [F3, F4]. On $V$ the primed component functions $F^{' a b} = Λ^{a}_{c} Λ^{b}_{d} F^{c d}$ and $j^{' a} = Λ^{a}_{b} j^{b}$ are constant-coefficient finite linear combinations of the unprimed component functions [F3], so $E^{'}, B^{'}$ inherit the joint class of $E, B$ under the fixed linear relabelling of the dictionary [F1], the additional derivatives required by each displayed equation exist and are continuous, and $ρ^{'}, J^{'}$ are continuous whenever $ρ, J$ are.

2.1givenstep 1.1step 1.2step 1.3F2F6algebra

(Clause (a′): arbitrary-direction boost) Let $v \in R^{3}$ with $∣ v ∣ < c$ . If $v = 0$ , then $B (0) = {id}_{V}$ [F2], the charts differ by the translation $x^{'} = x + b$ , the components are unchanged by [F3], so $E^{'} = E$ and $B^{'} = B$ , and the closed formulas reduce to the identity because $γ_{v} = 1$ and all terms carrying $v$ vanish; no parallel direction is needed. Let $v \neq 0$ and use $u, \hat{a}, b, S, R, β$ and the conjugation identity $B (v / c) = {\hat{R}}^{T} Λ_{β} \hat{R} = diag (1, S) Λ_{β} diag (1, R)$ of step 1.3. By [F3] the total component law of the composite is the matrix product of the factors of $B (v / c) = {\hat{R}}^{T} Λ_{β} \hat{R}$ ; applied successively, the first stage is the rotation $\hat{R} = diag (1, R)$ (step 1.2 with $A = R$ , whose hypotheses $R^{T} R = I_{3}$ and $\det R = 1$ hold by step 1.3), giving $E^{''} = R E$ , $B^{''} = R B$ ; the second stage is the axis boost $Λ_{β}$ in the intermediate frame, where step 1.1 applies because its proof uses only the dictionary and the component law; the third stage is the rotation ${\hat{R}}^{T} = diag (1, R^{T})$ (step 1.2 with $A = R^{T}$ , whose hypotheses $R R^{T} = I_{3}$ and $\det (R^{T}) = \det R = 1$ hold by step 1.3 and [F7]), giving $E^{'} = R^{T} E^{'''}$ and $B^{'} = R^{T} B^{'''}$ . Writing $∥, ⊥$ for the components along $e_{1}$ in the intermediate coordinates, step 1.1 applied in the intermediate frame gives $E^{'''} = E_{∥}^{''} + γ (E^{''} + β c e_{1} \times B^{''})_{⊥}$ and $B^{'''} = B_{∥}^{''} + γ (B^{''} - β c e_{1} \times E^{''} / c^{2})_{⊥}$ ; applying $S = R^{T}$ to the intermediate vectors and using the cross-product identity $R^{T} (p \times q) = (R^{T} p) \times (R^{T} q)$ for the orthogonal matrix $R$ (obtained from the identity of step 1.2 by applying $R$ to both sides: $R ((R^{T} p) \times (R^{T} q)) = (R R^{T} p) \times (R R^{T} q) = p \times q$ ) gives $R^{T} (E^{''} + β c e_{1} \times B^{''}) = E + β c (R^{T} e_{1}) \times (R^{T} B^{''}) = E + v \times B$ , since $R^{T} e_{1} = S e_{1} = u$ and $v = β c u$ ; moreover $R^{T} E_{∥}^{''} = (e_{1} \cdot E^{''}) R^{T} e_{1} = (u \cdot E) u = E_{∥}$ and $R^{T} B_{∥}^{''} = (u \cdot B) u = B_{∥}$ . Hence $E^{'} = E_{∥} + γ (E + v \times B)_{⊥}$ and $B^{'} = B_{∥} + γ (B - v \times E / c^{2})_{⊥}$ , which is the stated parallel/perpendicular form, and it yields $E_{∥}^{'} = E_{∥}$ , $B_{∥}^{'} = B_{∥}$ by taking inner products with $u$ . Finally $E_{∥} + γ (E + v \times B)_{⊥} = γ (E + v \times B) - (γ - 1) (u \cdot E) u$ and $(γ - 1) (u \cdot E) u = \frac{γ^{2}}{γ + 1} \frac{v (v \cdot E)}{c^{2}}$ , because $(u \cdot E) u = (v \cdot E) v / ∣ v ∣^{2}$ and $(γ - 1) / β^{2} = γ^{2} / (γ + 1)$ [F2]; the same computation for $B$ gives the displayed closed formulas for every $v \neq 0$ , with $γ_{v} = γ$ since $∣ v ∣ / c = β$ .

2.2givenstep 1.1F1F2algebra

(Clause (b): the invariants under the axis boost) Substituting the components of step 1.1, $∣ B^{'} ∣^{2} - \frac{∣ E^{'} ∣^{2}}{c^{2}} = B_{1}^{2} - \frac{E_{1}^{2}}{c^{2}} + γ^{2} [(B_{2} + β E_{3} / c)^{2} + (B_{3} - β E_{2} / c)^{2}] - \frac{γ^{2}}{c^{2}} [(E_{2} - β c B_{3})^{2} + (E_{3} + β c B_{2})^{2}]$ ; the linear terms cancel in pairs and the transverse contributions combine to $γ^{2} (1 - β^{2}) (B_{2}^{2} + B_{3}^{2} - (E_{2}^{2} + E_{3}^{2}) / c^{2}) = B_{2}^{2} + B_{3}^{2} - (E_{2}^{2} + E_{3}^{2}) / c^{2}$ because $γ^{2} (1 - β^{2}) = 1$ [F2], giving the first display. Likewise $E^{'} \cdot B^{'} = E_{1} B_{1} + γ^{2} [(E_{2} - β c B_{3}) (B_{2} + β E_{3} / c) + (E_{3} + β c B_{2}) (B_{3} - β E_{2} / c)] = E_{1} B_{1} + γ^{2} (1 - β^{2}) (E_{2} B_{2} + E_{3} B_{3}) = E \cdot B$ , since the mixed terms cancel in pairs. By [F1] the scalar fields $I_{1}$ and $I_{2}$ computed from the components in $x$ are $∣ B ∣^{2} - ∣ E ∣^{2} / c^{2}$ and $4 E \cdot B / c$ , and those computed from the components in $x^{'}$ are the same expressions in the primed fields, so the two displays say exactly that $I_{1}$ and $I_{2}$ take the same values in the two charts.

3.1givenstep 1.2step 2.1F3F4

(Clause (c): general proper orthochronous changes) Let $Λ$ be proper orthochronous with chart $x^{'} = Λ x + b$ . By [F3] the primed components are $F^{' a b} = Λ^{a}_{c} Λ^{b}_{d} F^{c d}$ , which is the first assertion. By [F4] there is a unique $β \in R^{3}$ with $∣ β ∣ < 1$ and a spatial rotation $R$ of the frame with $Λ = B (- β) \hat{R}$ . Taking the intermediate chart $x^{''} = \hat{R} x$ and the final chart $x^{'} = B (- β) x^{''} + b$ realizes the same transition $x^{'} = Λ x + b$ ; by step 1.2 the intermediate fields are $E^{''} = R E$ , $B^{''} = R B$ , and by step 2.1 applied with velocity $v = - c β$ — for which $∣ v ∣ = c ∣ β ∣ < c$ and $B (v / c) = B (- β)$ [F2] — the final fields are $E^{'} = E_{∥}^{''} + γ_{v} (E^{''} + v \times B^{''})_{⊥}$ and $B^{'} = B_{∥}^{''} + γ_{v} (B^{''} - v \times E^{''} / c^{2})_{⊥}$ , with $γ_{v} = (1 - ∣ v ∣^{2} / c^{2})^{- 1 / 2} = (1 - ∣ β ∣^{2})^{- 1 / 2}$ . This is exactly the statement that the change acts first by $(E, B) \mapsto (R E, R B)$ and then by the boost law (a′) with velocity $- c β$ ; the axis-only law of (a) was not substituted for it.

3.2givenstep 1.2step 2.1step 2.2F1F5F6

(Clause (b), general changes: the two scalar combinations) Every proper orthochronous change preserves $∣ B ∣^{2} - ∣ E ∣^{2} / c^{2}$ and $E \cdot B$ . Indeed, writing $Λ = B (- β) \hat{R}$ by [F4], the transformation factorizes into the rotation $\hat{R}$ , the axis boost $Λ_{β}$ in the intermediate frame and the inverse rotation, as in step 2.1; a spatial rotation with matrix $A$ satisfying $A^{T} A = I_{3}$ preserves the Euclidean norm and inner product of vectors, $∣ A E ∣^{2} = ∣ E ∣^{2}$ , $∣ A B ∣^{2} = ∣ B ∣^{2}$ and $(A E) \cdot (A B) = E \cdot B$ [F5]; and the axis boost preserves the two combinations $∣ B ∣^{2} - ∣ E ∣^{2} / c^{2}$ and $E \cdot B$ by step 2.2. Chaining the three stages gives the invariance for every proper orthochronous change, hence in particular for the boost chart $x^{'}$ of clause (b), and by [F1] the equivalently stated invariance of $I_{1}$ and $I_{2}$ .

4.1givenstep 1.4step 3.1F1F3F4F8F9

(Clause (d): form invariance of the smooth Maxwell branch) Let $x^{'} = Λ x + b$ with $Λ$ proper orthochronous, and assume that on $V$ the four smooth-branch equations of [F9] hold for $(E, B, ρ, J)$ . By [F8] the two tensor systems $(T M 1)$ and $(T M 2)$ hold in $x$ on $V$ and therefore also hold in $x^{'}$ on $V$ with the primed components of the same $F$ and the same four-current, and then the four smooth-branch equations hold in $x^{'}$ for the primed dictionary fields; the primed fields are exactly the fields $E^{'}, B^{'}$ read in the dictionary [F1], which by step 3.1 are the components of the same $F$ given by the component law, and the primed sources are $(c ρ^{'}, J^{'})$ because $j^{' a} = Λ^{a}_{b} j^{b}$ with $j^{0} = c ρ$ , $j^{i} = J^{i}$ [F3, F1]. The hypotheses of [F8] in the chart $x^{'}$ are met because the primed fields and sources are again of the required class on the open set $V$ by step 1.4. The converse is the same chain with the roles of $x$ and $x^{'}$ exchanged, since $Λ^{- 1}$ is again a proper orthochronous Lorentz matrix [F4].

5.1givenstep 1.1step 1.2step 1.3step 1.4step 2.1step 2.2step 3.1step 3.2step 4.1∎

(Hypotheses and scope) Clause (a) is step 1.1, clause (a′) is step 2.1, clause (b) is steps 2.2 and 3.2, clause (c) is steps 1.2 and 3.1, and clause (d) is step 4.1. The argument used only the component dictionary and invariants [F1], the two boost matrices and the identity $(γ - 1) / β^{2} = γ^{2} / (γ + 1)$ [F2], the constant component law and the invertibility of the changes of chart [F3, F4], the unique factorization of a proper orthochronous Lorentz map [F4], the matrix form and determinant of a spatial rotation [F5], the cross-product and Euclidean identities [F6], the determinant identities [F7], the tensor equivalence of [F8] and the smooth Maxwell branch [F9]. Only finitely many choices are made (the least index $j$ in step 1.3 and the finite index sets of [F7]); no choice principle, no potential, no derivative of the fields beyond the class required by the cited statements, no boundary, decay or medium hypothesis and no empirical premise are used. All clauses are pointwise on the open overlap of the two chart restrictions and conditional on the adopted postulates; orientation-reversing changes are outside the framework's conventions [F1], and no apparatus, detector or measurement model is introduced.

Source notes

The three cited treatments present the transformation of the fields under a passive boost, the rotation embedding and the two independent scalar contractions of the field tensor in their own conventions. The deduction above is the component computation in the framework's fixed dictionary (signs $F_{0 i} = - E_{i} / c$ , $F_{i j} = ϵ_{i j k} B_{k}$ , $x^{0} = c t$ , $η = diag (- 1, 1, 1, 1)$ ), the explicit conjugation of the general vector boost by a rotation, and the resulting invariance of the two scalar combinations and of the smooth Maxwell branch; the conversion from the sources' conventions is carried out here rather than assumed.

Covariance, boosts and the two field invariants

Statement

Facts & Assumptions

Proof

Source notes

Depends on

Dependency tree · 2 levels

Sources