Pipeline-generated

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.

Light and Doppler

1 · Prerequisites

2 · Summary

This page develops the wave and Doppler structure of the flat classical special-relativity model from explicit linear algebra on the affine Minkowski space, and then compares inertial descriptions of one ideal plane wave. The mathematical layer comes first. The metric pairing of a Lorentz vector space is a linear bijection onto the algebraic dual and supplies the raised covector $k^{♯}$ of a wave covector with its orthonormal-basis components (The metric pairing is a linear bijection to the dual, and the raised covector in an orthonormal frame); affine phase functions on affine Minkowski space, their level sets and kernels, and the terminology of null, future, past and causal wave covectors are fixed without any physical interpretation or units (Affine phase functions and wave covectors on affine Minkowski space). A future timelike vector pairs negatively with every nonzero future causal vector (A future timelike vector pairs negatively with every nonzero future causal vector), which is what makes the frame data $(ϖ, s)$ of a future null wave covector well defined with $ϖ > 0$ and $∣ s ∣ = 1$ and the raised vector the future null vector $ϖ (e_{0} + s)$ (Frame data of a future null wave covector: the unique pair $(ϖ, s)$ with $∣ s ∣ = 1$ ). The frame data transforms under a passive boost by the exact component law, the factor $ϖ^{'} = γ (1 - β \cdot s) ϖ$ and the direction formula (Boost transformation of a future null wave covector and of its frame data), and the phase rate along any future timelike worldline is the wave covector evaluated on the four-velocity, with $k (U) < 0$ for future null $k$ (The phase rate along a worldline is the wave covector evaluated on the four-velocity).

The physical vocabulary is then attached by definitions and an adopted model, not by deduction. The SI conventions give the angular frequency, linear frequency, wave vector, wavelength and propagation direction of a future null wave covector and the observer frequency $ω_{n} = - c k (n) = - k (U_{o})$ with the sign convention that makes it positive (Null wave covectors, frame frequency data and the observer frequency of an ideal plane wave); the ideal plane-wave model adopts the phase, wave-front, ray and reading assumptions explicitly, with its exclusions listed (Adopted ideal plane-wave and frequency-reading model). Conditionally on that model, one ideal wave between two inertial descriptions related by a boost has the transformed frame data and the frequency and wavelength ratios, the two longitudinal shifts, both transverse protocols with their different factors $γ$ and $1 / γ$ , and the aberration law $\cos θ^{'} = (\cos θ - ∣ β ∣) / (1 - ∣ β ∣ \cos θ)$ (Doppler shift and aberration for an ideal plane wave between inertial descriptions). A closing remark fixes the units, the two coordinate forms and the natural-unit restoration table (Units, coordinate conventions and c restoration for the wave and Doppler formulas).

Nothing on this page measures anything. The postulates are adopted idealizations, the theorem is a conditional deduction from them, and its exclusions (media, dispersion, modulation, intensity, polarization, sources, detectors, accelerating observers, gravitation and quantum effects) travel to every consumer. Empirical tests of the model belong to the framework's experimental work. The companion page works the transformations out at $β = 3 / 5$ and refutes one universal transverse-Doppler claim.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

LemmaStatement: AI-adaptedProof: AI-adaptedjudge pass (gpt-6.1-sol)Open item page →

The metric pairing is a linear bijection to the dual, and the raised covector in an orthonormal frame

Statement

Let $(V, η)$ be a $4$ -dimensional Lorentz vector space (Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space): $η$ is symmetric and bilinear, nondegenerate in the sense that both radicals are ${0}$ (The matrix, left and right radicals, rank, and nondegeneracy of a bilinear form on a finite-dimensional space), and of inertia $(3, 1, 0)$ . Let $V^{*}$ be the algebraic dual (Linear functionals and the algebraic dual $V^{*} = L (V, F)$ ). Then:

(a) The map $Φ : V \to V^{*}$ , $Φ (v) (w) : = η (v, w)$ , is linear, and it is injective: $Φ (v) = 0$ means $η (v, w) = 0$ for all $w \in V$ , that is $v \in {rad}_{L} (η) = {0}$ .

(b) $\dim V^{*} = \dim V = 4$ (The dual family of a finite basis is a basis of the dual space, with the same dimension), so $Φ$ is a linear bijection; equivalently $nullity Φ = 0$ and $rank Φ = 4$ (Rank-nullity: $\dim_{F} V = nullity T + rank T$ , Rank and nullity of a linear map with finite-dimensional domain).

(c) Consequently for every covector $k \in V^{*}$ there is a unique vector $k^{♯} \in V$ with $η (k^{♯}, w) = k (w)$ for all $w \in V$ ; the assignment $♯ : V^{*} \to V$ , $k \mapsto k^{♯}$ , is linear and is the inverse of $Φ$ (Invertible linear maps, linear isomorphisms, and inverse linear maps), so $(v^{♭})^{♯} = v$ for $v^{♭} : = Φ (v)$ and $(k^{♯})^{♭} = k$ for every $k \in V^{*}$ ; in particular $k^{♯} = 0$ if and only if $k = 0$ .

(d) If $(e_{0}, e_{1}, e_{2}, e_{3})$ is an $η$ -orthonormal ordered basis of $V$ (Every Lorentz form admits an ordered basis with matrix diag(-1,1,1,1)) and $k_{a} : = k (e_{a})$ are the values of $k$ on that basis, then

$k^{♯} = - k_{0} e_{0} + k_{1} e_{1} + k_{2} e_{2} + k_{3} e_{3},$

that is $(k^{♯})^{0} = - k_{0}$ and $(k^{♯})^{i} = k_{i}$ for $i = 1, 2, 3$ in this basis, and

$η (k^{♯}, k^{♯}) = - (k_{0})^{2} + (k_{1})^{2} + (k_{2})^{2} + (k_{3})^{2} .$

Hence, for $k \neq 0$ the vector $k^{♯}$ is nonzero and, in the sense of (Timelike, null, spacelike and causal vectors of a Lorentz vector space), it is null exactly when $(k_{0})^{2} = (k_{1})^{2} + (k_{2})^{2} + (k_{3})^{2}$ , timelike exactly when $(k_{0})^{2} > (k_{1})^{2} + (k_{2})^{2} + (k_{3})^{2}$ (equivalently $η (k^{♯}, k^{♯}) < 0$ ), and spacelike exactly when $(k_{0})^{2} < (k_{1})^{2} + (k_{2})^{2} + (k_{3})^{2}$ (equivalently $η (k^{♯}, k^{♯}) > 0$ ); for $k = 0$ one has $k^{♯} = 0$ , which has no causal character.

No orientation, time orientation or affine structure is used, and no choice principle is used.

Facts & Assumptions

Given: A $4$ -dimensional real vector space $V$ , a Lorentz form $η$ on $V$ , and the map $Φ (v) : = η (v, \cdot)$ .

[L1]

$V$ is $4$ -dimensional, and $η$ is symmetric and bilinear with ${rad}_{L} (η) = {rad}_{R} (η) = {0}$ and inertia $(3, 1, 0)$ (Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space, The matrix, left and right radicals, rank, and nondegeneracy of a bilinear form on a finite-dimensional space).

[L2]

$V^{*} = L (V, R)$ is the algebraic dual of $V$ , and the assignment $B \mapsto B^{♭}$ with $B^{♭} (v) (w) = B (v, w)$ is a linear bijection from the bilinear forms on $V$ onto $L (V, V^{*})$ ; in particular $B^{♭}$ is a linear map for every bilinear form $B$ (Linear functionals and the algebraic dual $V^{*} = L (V, F)$ , Bilinear forms on $V$ correspond linearly and bijectively to linear maps $V \to V^{*}$ , Linear map between vector spaces over the same field).

[L3]

If $B = (b_{1}, \dots, b_{n})$ is a basis of a finite-dimensional $F$ -vector space, then its dual family is a basis of the dual space; consequently $\dim V^{*} = \dim V$ (The dual family of a finite basis is a basis of the dual space, with the same dimension).

[L4]

There is an $η$ -orthonormal ordered basis $(e_{0}, e_{1}, e_{2}, e_{3})$ of $V$ , that is, $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)_{a b}$ for all $a, b$ (Every Lorentz form admits an ordered basis with matrix diag(-1,1,1,1)).

[L5]

For a linear map $T$ with finite-dimensional domain, $\dim V = nullity T + rank T$ , where $nullity T = \dim (\ker T)$ and $rank T = \dim (im T)$ (Rank-nullity: $\dim_{F} V = nullity T + rank T$ , Rank and nullity of a linear map with finite-dimensional domain).

[L6]

A linear map $T$ is invertible, equivalently a linear isomorphism, when there is a linear map $S$ with $S \circ T = id$ and $T \circ S = id$ ; such an $S$ is unique and written $T^{- 1}$ , and $T$ is bijective (Invertible linear maps, linear isomorphisms, and inverse linear maps).

[L7]

A vector $v \in V$ is timelike, null or spacelike according as $η (v, v) < 0$ , $η (v, v) = 0$ with $v \neq 0$ , or $η (v, v) > 0$ ; the zero vector has none of these characters, and every nonzero vector has exactly one (Timelike, null, spacelike and causal vectors of a Lorentz vector space).

Proof

technique · direct

1.1L1L2given

The map $Φ$ is linear, and $\ker Φ = {0}$ . Since $η$ is a bilinear form on $V$ , its associated map $η^{♭}$ lies in $L (V, V^{*})$ and $η^{♭} (v) (w) = η (v, w) = Φ (v) (w)$ for all $v, w$ , so $Φ = η^{♭}$ is linear by [L2]. If $Φ (v) = 0$ , then $η (v, w) = 0$ for every $w \in V$ , so $v$ lies in the left radical of $η$ , which is ${0}$ by [L1]; conversely $Φ (0) = 0$ by linearity (equivalently $η (0, \cdot) = 0$ ), so $\ker Φ = {0}$ .

1.2L3L4algebra

The map $Φ$ is surjective. Fix an $η$ -orthonormal ordered basis $(e_{0}, e_{1}, e_{2}, e_{3})$ of $V$ [L4], with dual family $(e^{0}, e^{1}, e^{2}, e^{3})$ , a basis of $V^{*}$ by [L3]. For all $a, b$ one has $Φ (e_{a}) (e_{b}) = η (e_{a}, e_{b}) = η_{a a} δ_{a b}$ with $η_{a a} \in {- 1, 1}$ , by [L4], and the functional $η_{a a} e^{a}$ takes the same values on the basis $(e_{b})$ ; two linear functionals that agree on a basis agree on every vector, so $Φ (e_{a}) = η_{a a} e^{a}$ , which exhibits $e^{a} = η_{a a} Φ (e_{a})$ as a scalar multiple of $Φ (e_{a})$ (here $η_{a a}^{- 1} = η_{a a}$ ). Hence every element of the basis $(e^{a})$ of $V^{*}$ lies in the linear span of $Φ (e_{0}), \dots, Φ (e_{3})$ , so that span is all of $V^{*}$ ; therefore $Φ$ is surjective.

2.1step 1.1step 1.2L1L3L5L6

The map $Φ$ is a linear bijection, $\dim V^{*} = \dim V = 4$ , and the inverse assignment $♯$ exists with the stated properties. By step 1.1 $Φ$ is injective and by step 1.2 it is surjective, hence bijective; by [L3] and [L1], $\dim V^{*} = \dim V = 4$ ; and [L5] applied to the linear map $Φ$ gives the same picture independently, $nullity Φ = \dim \ker Φ = 0$ and $rank Φ = 4 = \dim V^{*}$ , with $rank Φ = \dim im Φ$ and $im Φ = V^{*}$ by step 1.2. By [L6] the inverse $Φ^{- 1} : V^{*} \to V$ is a well-defined linear map, unique, and satisfies $Φ^{- 1} \circ Φ = {id}_{V}$ and $Φ \circ Φ^{- 1} = {id}_{V^{*}}$ . Writing $k^{♯} : = Φ^{- 1} (k)$ for $k \in V^{*}$ , we get $η (k^{♯}, w) = Φ (k^{♯}) (w) = k (w)$ for every $w \in V$ ; any $c$ with $η (c, w) = k (w)$ for all $w$ satisfies $Φ (c) = k$ , hence $c = k^{♯}$ by injectivity of $Φ$ , which is the asserted uniqueness. The two inverse equations are exactly $(v^{♭})^{♯} = v$ for $v^{♭} = Φ (v)$ and $(k^{♯})^{♭} = k$ , and $k^{♯} = 0$ holds if and only if $k = Φ (k^{♯}) = Φ (0) = 0$ . This proves (a), (b) and (c).

3.1step 1.2step 2.1L1L4algebra

Component formula. Let $k \in V^{*}$ and keep the orthonormal basis $(e_{a})$ of step 1.2; put $c^{0} : = - k_{0}$ and $c^{i} : = k_{i}$ for $i = 1, 2, 3$ , where $k_{a} = k (e_{a})$ , and set $c : = c^{0} e_{0} + c^{1} e_{1} + c^{2} e_{2} + c^{3} e_{3}$ . For every basis vector $e_{b}$ , bilinearity and orthonormality [L1, L4] give $η (c, e_{b}) = \sum_{a} c^{a} η (e_{a}, e_{b}) = c^{b} η_{b b}$ ; hence $η (c, e_{0}) = - c^{0} = k_{0} = k (e_{0})$ and $η (c, e_{i}) = c^{i} = k_{i} = k (e_{i})$ for $i = 1, 2, 3$ . The functionals $w \mapsto η (c, w)$ (linear in its second argument by [L1]) and $k$ agree on the basis $(e_{b})$ , hence on all of $V$ ; therefore $Φ (c) = k$ , and uniqueness in step 2.1 yields $c = k^{♯} = - k_{0} e_{0} + k_{1} e_{1} + k_{2} e_{2} + k_{3} e_{3}$ .

4.1step 2.1step 3.1L4L7∎

Quadratic form and causal trichotomy. With $k^{♯} = \sum_{a} c^{a} e_{a}$ from step 3.1, bilinearity and orthonormality give $η (k^{♯}, k^{♯}) = \sum_{a, b} c^{a} c^{b} η (e_{a}, e_{b}) = \sum_{a} (c^{a})^{2} η_{a a} = - (c^{0})^{2} + (c^{1})^{2} + (c^{2})^{2} + (c^{3})^{2} = - (k_{0})^{2} + (k_{1})^{2} + (k_{2})^{2} + (k_{3})^{2}$ , because $(c^{0})^{2} = (k_{0})^{2}$ and $c^{i} = k_{i}$ . If $k \neq 0$ then $k^{♯} \neq 0$ by step 2.1, so [L7] applies: $k^{♯}$ is null exactly when this value is $0$ , that is when $(k_{0})^{2} = (k_{1})^{2} + (k_{2})^{2} + (k_{3})^{2}$ ; timelike exactly when it is negative, that is when $(k_{0})^{2} > (k_{1})^{2} + (k_{2})^{2} + (k_{3})^{2}$ ; and spacelike exactly when it is positive, that is when $(k_{0})^{2} < (k_{1})^{2} + (k_{2})^{2} + (k_{3})^{2}$ . If $k = 0$ then $k^{♯} = 0$ by step 2.1 and the zero vector has no causal character by [L7]. No orientation, time orientation or affine structure was used, and no choice principle was used.

DefinitionDefinition: AI-adaptedProof: AI-adaptedjudge pass (gpt-6.1-sol)Open item page →

Affine phase functions and wave covectors on affine Minkowski space

Definition

Let $(A, V, η, C^{+})$ be the oriented time-oriented affine Minkowski space (Oriented time-oriented affine Minkowski space (the spacetime primitives)), with displacements $q - p \in V$ (Affine spaces over a real vector space and displacement vectors).

(a) Affine phase functions. A map $θ : A \to R$ is an affine phase function when there are $q \in A$ and a covector $k \in V^{*}$ (Linear functionals and the algebraic dual $V^{*} = L (V, F)$ ) with

$θ (p) - θ (q) = k (p - q) for all p \in A .$

The covector $k$ is then unique: if $k^{'}$ also satisfies the identity, then $(k - k^{'}) (p - q) = 0$ for all $p \in A$ , and as $p$ runs over $A$ the displacements $p - q$ run over all of $V$ , so $k - k^{'} = 0$ as a functional. This unique covector is the differential $d θ$ of $θ$ ; when $k \neq 0$ , it is also called the wave covector of $θ$ , as in clause (c). Conversely, for every $q \in A$ , every $k \in V^{*}$ and every $θ_{0} \in R$ , the formula

$θ (p) : = k (p - q) + θ_{0}$

defines an affine phase function with $d θ = k$ and $θ (q) = θ_{0}$ ; hence for each fixed $q$ the map $θ \mapsto (d θ, θ (q))$ is a bijection from the set of affine phase functions onto $V^{*} \times R$ . In the inertial chart $x$ of an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ (Inertial frames and inertial charts of the affine Minkowski model), writing $k_{a} : = k (e_{a})$ , one has

$θ (p) = k_{a} x^{a} (p) + θ (o)$

because $p - o = \sum_{a} x^{a} (p) e_{a}$ with unique coordinates $x^{a} (p)$ (A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis) and $k$ is linear; for a second origin $o^{'}$ one has $θ (o^{'}) = θ (o) + k (o^{'} - o)$ .

(b) Constant-phase directions and level sets. For $v \in V$ , $p \in A$ and $s \in R$ one has $θ (p + s v) = θ (p) + s k (v)$ by the defining identity, so $k (v) = 0$ if and only if $θ$ is constant on the line $p + R v$ for every $p \in A$ . If $k \neq 0$ , the direction subspace

$\ker k : = {v \in V : k (v) = 0}$

is a $3$ -dimensional linear subspace of $V$ : it is the kernel of the nonzero linear functional $k$ , and choosing $v_{0}$ with $k (v_{0}) \neq 0$ gives every $v \in V$ the unique decomposition $v = (k (v) / k (v_{0})) v_{0} + w$ with $w \in \ker k$ , so $V = \ker k \oplus R v_{0}$ and $\dim \ker k = 4 - 1 = 3$ ; every nonempty level set

$Σ_{t} : = {p \in A : θ (p) = t}$

is then the affine hyperplane $p_{0} + \ker k$ through any of its points $p_{0}$ , and the level set is empty when $t$ is not a value of $θ$ . If $k = 0$ then $θ$ is constant and $Σ_{t}$ is either empty or all of $A$ . For the derivative assertion, $I \subseteq R$ is an order-convex set with at least two points, and a $C^{1}$ curve $γ : I \to A$ means a map whose four real components in an inertial chart are differentiable with continuous derivatives, using one-sided derivatives at included endpoints. Its tangent $γ^{'} (s)$ is the vector with those component derivatives in the frame basis; equivalently it is the limit in frame coordinates of $(γ (s + h) - γ (s)) / h$ . This definition and tangent are independent of the inertial chart: chart transitions are affine with invertible constant linear part, and finite linear combinations preserve derivatives and their continuity by 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 Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function. Finally, for every such $C^{1}$ curve $γ : I \to A$ one has $(θ \circ γ)^{'} (s) = k (γ^{'} (s))$ for all $s \in I$ : in the coordinates of any inertial chart this is the identity $\frac{d}{d s} (k_{a} x^{a} (γ (s)) + θ (o)) = \sum_{a} k_{a} \frac{d}{d s} x^{a} (γ (s))$ . The sum and scalar-multiple rules of 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$ , iterated over the four components, and the zero difference quotient of the constant $θ (o)$ justify this equality, including one-sided endpoints. Its right-hand side is the same linear combination read in the coordinates of $γ^{'} (s)$ .

(c) Wave covectors. A wave covector on $(A, V, η)$ is a nonzero element $k \in V^{*}$ . With $k^{♯}$ the raised vector of The metric pairing is a linear bijection to the dual, and the raised covector in an orthonormal frame (so that $η (k^{♯}, w) = k (w)$ for all $w \in V$ , and $k^{♯} = 0$ exactly when $k = 0$ ), the covector $k$ is called null, timelike or spacelike when $η (k^{♯}, k^{♯})$ is zero, negative or positive, and future, past, future null, past null or causal when $k^{♯}$ is respectively future causal, past causal, future null, past null or causal in the sense of Timelike, null, spacelike and causal vectors of a Lorentz vector space and Time orientation, future and past timelike/null/causal vectors, and the closed cones; a future null wave covector is one that is both future and null. These terms are well posed: a wave covector has $k \neq 0$ , hence $k^{♯} \neq 0$ , and a nonzero vector has exactly one causal character and is future or past exactly when it is causal.

(d) Mathematical scope. This item introduces mathematical objects and terminology only. It excludes the zero covector from the term wave covector, it fixes no units and no physical interpretation, and it does not claim that light or any physical wave is described by such a phase; that identification is adopted in post-sr-ideal-plane-wave-model. No choice principle is used.

LemmaStatement: AI-adaptedProof: AI-adaptedOpen item page →

A future timelike vector pairs negatively with every nonzero future causal vector

Statement

Let $(A, V, η, C^{+})$ be the oriented time-oriented affine Minkowski space, let $n, v \in V$ , and recall that a nonzero $v$ with $η (v, v) \leq 0$ is causal (Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones). Then:

(a) if $n$ is future timelike and $v$ is nonzero future causal, then $η (n, v) < 0$ ;

(b) if $n$ is future timelike and $v$ is nonzero past causal, then $η (n, v) > 0$ ;

(c) consequently, for a nonzero null vector $v$ and any future timelike $n$ , $v$ is future null if and only if $η (n, v) < 0$ , and $v$ is past null if and only if $η (n, v) > 0$ ; the sign of $η (n, v)$ does not depend on the choice of the future timelike $n$ ;

(d) if $n_{h a t} : = n / \sqrt{- η (n, n)}$ is the normalization of a future timelike $n$ , then $n_{h a t}$ is future unit timelike, $η (n_{h a t}, n_{h a t}) = - 1$ , and $η (n, v) = \sqrt{- η (n, n)} η (n_{h a t}, v)$ for every $v$ , so the sign statements hold for $n_{h a t}$ as well.

The statement is pure affine Minkowski geometry, and no choice principle is used.

Facts & Assumptions

Given: An oriented time-oriented affine Minkowski space $(A, V, η, C^{+})$ and vectors $n, v \in V$ .

[L1]

A vector is timelike when $η (v, v) < 0$ , null when $v \neq 0$ and $η (v, v) = 0$ , spacelike when $η (v, v) > 0$ , and causal when it is timelike or null; the zero vector has no causal character and every nonzero vector has exactly one character (Timelike, null, spacelike and causal vectors of a Lorentz vector space).

[L2]

$C^{+}$ is one of the two connected components of the timelike set, and future timelike means membership in $C^{+}$ , future null means nonzero null membership in $cl (C^{+})$ , and future causal means future timelike or future null; the closed cones $cl (C^{+})$ and $cl (C^{-})$ are convex cones meeting only at $0$ , and every causal vector is future or past but not both (Time orientation, future and past timelike/null/causal vectors, and the closed cones).

[L3]

In an $η$ -orthonormal basis $(e_{0}, e_{1}, e_{2}, e_{3})$ with $e_{0}$ timelike, writing $x = x^{0} e_{0} + x_{v e c}$ with $x_{v e c} : = \sum_{i = 1}^{3} x^{i} e_{i} \in span (e_{1}, e_{2}, e_{3})$ and $∣ x_{v e c} ∣ : = \sqrt{(x^{1})^{2} + (x^{2})^{2} + (x^{3})^{2}}$ and $η_{00} : = η (e_{0}, e_{0}) = - 1$ , the timelike set splits into $T_{+} = {x : x^{0} > ∣ x_{v e c} ∣}$ and $T_{-} = {x : x^{0} < - ∣ x_{v e c} ∣}$ , these are exactly its two connected components, $cl (T_{+}) = {x : x^{0} \geq ∣ x_{v e c} ∣}$ and $cl (T_{-}) = {x : x^{0} \leq - ∣ x_{v e c} ∣}$ (The timelike set has exactly two convex components, described in orthonormal coordinates).

[L4]

For every event $o \in A$ there is an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ , so its ordered basis is $η$ -orthonormal with $e_{0} \in C^{+}$ (Existence of future-oriented inertial frames at every event, Inertial frames and inertial charts of the affine Minkowski model).

[L5]

For an inertial frame, with $S = span (e_{1}, e_{2}, e_{3})$ and $δ : S \times S \to R$ , $δ (w, z) : = η (w, z)$ , the positive-definite spatial form, the spatial vectors $x_{v e c} = \sum_{i = 1}^{3} x^{i} e_{i}$ and $y_{v e c} = \sum_{i = 1}^{3} y^{i} e_{i}$ belong to $S$ and satisfy $δ (x_{v e c}, y_{v e c}) = \sum_{i = 1}^{3} x^{i} y^{i}$ and $∣ x_{v e c} ∣ = \sqrt{δ (x_{v e c}, x_{v e c})}$ ; bilinearity and $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)$ give $η (x, y) = - x^{0} y^{0} + δ (x_{v e c}, y_{v e c})$ (The Euclidean spatial structure and cross product of an inertial frame).

[L6]

For real lists, $∣ \sum_{k < n} a_{k} b_{k} ∣ \leq \sqrt{\sum_{k < n} a_{k}^{2}} \sqrt{\sum_{k < n} b_{k}^{2}}$ (The Cauchy-Schwarz inequality for finite sums), which in the coordinates of [L5] reads $∣ δ (x_{v e c}, y_{v e c}) ∣ \leq ∣ x_{v e c} ∣ ∣ y_{v e c} ∣$ .

Proof

technique · direct

1.1L2L3L4L5L6

Frame and coordinates. Fix an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ [L4] and write every $x \in V$ as $x = x^{0} e_{0} + x_{v e c}$ , where $x_{v e c} : = \sum_{i = 1}^{3} x^{i} e_{i} \in S$ ; then $η (x, y) = - x^{0} y^{0} + δ (x_{v e c}, y_{v e c})$ with $∣ δ (x_{v e c}, y_{v e c}) ∣ \leq ∣ x_{v e c} ∣ ∣ y_{v e c} ∣$ by [L5, L6]. Because $e_{0} \in C^{+}$ and $e_{0} \in T_{+}$ , the component $T_{+}$ of [L3] is $C^{+}$ , so $C^{+} = {x : x^{0} > ∣ x_{v e c} ∣}$ and $cl (C^{+}) = cl (T_{+}) = {x : x^{0} \geq ∣ x_{v e c} ∣}$ [L2, L3].

2.1step 1.1

Clause (a). Let $n$ be future timelike and $v \neq 0$ future causal. By [L2] and step 1.1 the future causal vectors are $C^{+} \cup (cl (C^{+}) ∖ {0})$ , so in the frame of step 1.1, $n^{0} > ∣ n_{v e c} ∣$ and $v^{0} \geq ∣ v_{v e c} ∣ \geq 0$ ; $v \neq 0$ rules out $v^{0} = 0$ , so $v^{0} > 0$ . Then $η (n, v) = - n^{0} v^{0} + δ (n_{v e c}, v_{v e c}) \leq - n^{0} v^{0} + ∣ n_{v e c} ∣ ∣ v_{v e c} ∣ \leq - n^{0} v^{0} + ∣ n_{v e c} ∣ v^{0} = - (n^{0} - ∣ n_{v e c} ∣) v^{0} < 0$ , because $∣ v_{v e c} ∣ \leq v^{0}$ , $∣ n_{v e c} ∣ \geq 0$ , $n^{0} - ∣ n_{v e c} ∣ > 0$ and $v^{0} > 0$ .

3.1step 2.1L2L3

Clause (b). If $n$ is future timelike and $v$ is nonzero past causal, then $- v$ is nonzero future causal: $v \in C^{-}$ or $v$ is past null, and negating does not change $η (v, v)$ , while $cl (C^{-}) = - cl (C^{+})$ and $T_{-} = - T_{+}$ show $- v$ lies in $C^{+}$ (timelike case) or is nonzero null in $cl (C^{+})$ (null case) [L2, L3]. By step 2.1, $η (n, - v) < 0$ , and bilinearity gives $η (n, - v) = - η (n, v)$ , so $η (n, v) > 0$ .

4.1step 2.1step 3.1L1L2

Clause (c). Let $v$ be nonzero null and $n$ future timelike. If $v$ is future null then $v$ is nonzero future causal and step 2.1 gives $η (n, v) < 0$ ; if $v$ is past null then step 3.1 gives $η (n, v) > 0$ . Since a causal vector is future or past but not both [L2] and a nonzero null vector is causal, exactly one of these two cases occurs, so conversely $η (n, v) < 0$ forces $v$ future null and $η (n, v) > 0$ forces $v$ past null; the sign is therefore determined by $v$ alone and is independent of the future timelike $n$ used.

5.1step 1.1step 2.1step 3.1step 4.1L1∎

Clause (d). For future timelike $n$ , $- η (n, n) > 0$ by [L1], so $λ : = \sqrt{- η (n, n)}$ is a positive real number and $n_{h a t} : = n / λ$ is defined. By step 1.1, $n^{0} > ∣ n_{v e c} ∣ \geq 0$ ; multiplying by $λ^{- 1} > 0$ gives $n_{h a t}^{0} > ∣ n_{h a t, v e c} ∣$ , so $n_{h a t} \in T_{+} = C^{+}$ is future timelike; bilinearity gives $η (n_{h a t}, n_{h a t}) = λ^{- 2} η (n, n) = - 1$ and $η (n, v) = η (λ n_{h a t}, v) = λ η (n_{h a t}, v)$ for every $v$ . Hence $η (n_{h a t}, v)$ has the same sign as $η (n, v)$ for every $v$ , and the sign statements of steps 2.1, 3.1 and 4.1 hold with $n$ replaced by $n_{h a t}$ ; this proves (a)-(d). The argument used only the affine Minkowski geometry of the cited items, and no choice principle was used.

LemmaStatement: AI-adaptedProof: AI-adaptedOpen item page →

Frame data of a future null wave covector: the unique pair $(ϖ, s)$ with $∣ s ∣ = 1$

Statement

Let $(A, V, η, C^{+})$ be the oriented time-oriented affine Minkowski space, let $k$ be a future null wave covector (Affine phase functions and wave covectors on affine Minkowski space) and let $(o; e_{0}, e_{1}, e_{2}, e_{3})$ be an inertial frame with inertial chart $x$ (Inertial frames and inertial charts of the affine Minkowski model). Define

$ϖ : = - k (e_{0}), s_{i} : = \frac{k (e_{i})}{ϖ} (i = 1, 2, 3),$

and write $s : = (s_{1}, s_{2}, s_{3}) \in R^{3}$ with Euclidean norm $∣ s ∣$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ). Then:

(a) $ϖ > 0$ ;

(b) $∣ s ∣ = 1$ ;

(c) for every $v = v^{0} e_{0} + v^{1} e_{1} + v^{2} e_{2} + v^{3} e_{3}$ in $V$ one has $k (v) = ϖ (- v^{0} + s_{1} v^{1} + s_{2} v^{2} + s_{3} v^{3})$ ; equivalently the components of $k$ in the frame are $(k_{0}, k_{1}, k_{2}, k_{3}) = (- ϖ, ϖ s_{1}, ϖ s_{2}, ϖ s_{3})$ ;

(d) the raised vector is $k^{♯} = ϖ (e_{0} + s_{1} e_{1} + s_{2} e_{2} + s_{3} e_{3})$ , with frame coordinates $ϖ (1, s_{1}, s_{2}, s_{3})$ ; it is nonzero and future null, and $k (k^{♯}) = η (k^{♯}, k^{♯}) = 0$ ;

(e) conversely, if a covector $k \in V^{*}$ has frame components $(- ϖ, ϖ s_{1}, ϖ s_{2}, ϖ s_{3})$ with $ϖ > 0$ and $∣ s ∣ = 1$ in some inertial frame, then $k$ is a future null wave covector, and the construction of (a)-(b) applied to $k$ in that frame returns the same $ϖ$ and $s$ ;

(f) the pair $(ϖ, s)$ is uniquely determined by $k$ and the frame, and two future null wave covectors with the same pair agree; it is thus the complete frame description of a future null wave covector.

No choice principle is used.

Facts & Assumptions

Given: An oriented time-oriented affine Minkowski space $(A, V, η, C^{+})$ , a future null wave covector $k$ , and an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ .

[L1]

A wave covector is a nonzero element of $V^{*}$ ; it is future null if and only if its raised vector is future null (Affine phase functions and wave covectors on affine Minkowski space, clause (c)). Thus the given $k$ satisfies $k^{♯} \neq 0$ and $η (k^{♯}, k^{♯}) = 0$ . Metric duality gives $k (w) = η (k^{♯}, w)$ for every $w \in V$ (The metric pairing is a linear bijection to the dual, and the raised covector in an orthonormal frame, clause (c)).

[L2]

An inertial frame has $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)_{a b}$ , with $e_{0}$ future ( $e_{0} \in C^{+}$ ), and its vectors are linearly independent with every vector having unique coordinates in the basis (Inertial frames and inertial charts of the affine Minkowski model, A finite list $v : n \to V$ is an ordered basis if and only if every $x \in V$ equals $\sum_{i < n} λ_{i} v_{i}$ for exactly one $λ : n \to F$ ; those scalars are the coordinates of $x$ in that ordered basis).

[L3]

If $n$ is future timelike and $v$ is nonzero future causal, then $η (n, v) < 0$ (A future timelike vector pairs negatively with every nonzero future causal vector, clause (a)).

[L4]

A nonzero vector has exactly one causal character, and it is causal exactly when it is timelike or null; a causal vector is future or past but not both; future causal means future timelike or future null, and future null means nonzero null in $cl (C^{+})$ (Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones).

[L5]

In the frame, put $S : = span (e_{1}, e_{2}, e_{3})$ and write $v = v^{0} e_{0} + v_{v e c}$ , where $v_{v e c} : = \sum_{i = 1}^{3} v^{i} e_{i} \in S$ ; define $w_{v e c}$ likewise. For the positive-definite spatial form $δ : S \times S \to R$ , $η (v, w) = - v^{0} w^{0} + δ (v_{v e c}, w_{v e c})$ and $δ (v_{v e c}, w_{v e c}) = \sum_{i = 1}^{3} v^{i} w^{i}$ , so $∣ v_{v e c} ∣^{2} = \sum_{i = 1}^{3} (v^{i})^{2}$ (The Euclidean spatial structure and cross product of an inertial frame).

[L6]

For the components $k_{a} : = k (e_{a})$ of a covector, the raised vector is $k^{♯} = - k_{0} e_{0} + k_{1} e_{1} + k_{2} e_{2} + k_{3} e_{3}$ , and in the frame $η (k^{♯}, k^{♯}) = - (k_{0})^{2} + (k_{1})^{2} + (k_{2})^{2} + (k_{3})^{2}$ (The metric pairing is a linear bijection to the dual, and the raised covector in an orthonormal frame, clause (d)).

[L7]

The frame's first vector is future, so $C^{+} = {v : v^{0} > ∣ v_{v e c} ∣}$ and $cl (C^{+}) = {v : v^{0} \geq ∣ v_{v e c} ∣}$ (The timelike set has exactly two convex components, described in orthonormal coordinates).

[L8]

$∣ s ∣^{2} = \sum_{i} s_{i}^{2}$ for the Euclidean norm on $R^{3}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

Proof

technique · direct

1.1L1L2L3

Clause (a). Since $e_{0}$ is future and $η (e_{0}, e_{0}) = - 1$ , it is future timelike, and $k^{♯}$ is nonzero future causal by [L1]; [L3] gives $η (e_{0}, k^{♯}) < 0$ . By [L1] and symmetry of $η$ , $k (e_{0}) = η (k^{♯}, e_{0}) = η (e_{0}, k^{♯}) < 0$ , so $ϖ = - k (e_{0}) > 0$ .

1.2L2

Clause (c). For $v = \sum_{a} v^{a} e_{a}$ with unique coordinates and $k$ linear [L2], $k (v) = \sum_{a} v^{a} k (e_{a}) = v^{0} k (e_{0}) + \sum_{i} v^{i} k (e_{i}) = - ϖ v^{0} + \sum_{i} ϖ s_{i} v^{i} = ϖ (- v^{0} + s_{1} v^{1} + s_{2} v^{2} + s_{3} v^{3})$ , using the definitions of $ϖ$ and $s_{i}$ ; the component statement is the same identity read on the basis.

1.3L1L4L5L6L7L8

Clause (e). Let $k$ have components $(- ϖ, ϖ s_{1}, ϖ s_{2}, ϖ s_{3})$ with $ϖ > 0$ and $∣ s ∣ = 1$ in the given inertial frame. Then $k (e_{0}) = - ϖ \neq 0$ , so $k \neq 0$ ; by [L6], $k^{♯} = - k_{0} e_{0} + \sum_{i} k_{i} e_{i} = ϖ (e_{0} + s_{1} e_{1} + s_{2} e_{2} + s_{3} e_{3})$ . Its frame coordinates are $ϖ (1, s)$ , so $v : = k^{♯}$ satisfies $v^{0} = ϖ = ϖ ∣ s ∣ \geq 0$ and $∣ v_{v e c} ∣ = ϖ ∣ s ∣ = ϖ = v^{0}$ by [L5, L8]; hence $v \in cl (C^{+}) ∖ {0}$ by [L7], and $η (v, v) = - ϖ^{2} + ϖ^{2} ∣ s ∣^{2} = 0$ by [L5, L6, L8], so $v$ is null; by [L4] $v$ is future null, and by [L1] the nonzero covector $k$ is a future null wave covector. The construction of (a)-(b) returns $- k (e_{0}) = ϖ$ and $k (e_{i}) / ϖ = ϖ s_{i} / ϖ = s_{i}$ .

2.1step 1.1L2L6L8

Clause (b). By [L6], $k^{♯} = - k_{0} e_{0} + k_{1} e_{1} + k_{2} e_{2} + k_{3} e_{3}$ with $k_{0} = k (e_{0}) = - ϖ$ and $k_{i} = k (e_{i}) = ϖ s_{i}$ , so $k^{♯} = ϖ e_{0} + \sum_{i} ϖ s_{i} e_{i}$ . Orthonormality of the frame [L2] and bilinearity give $η (k^{♯}, k^{♯}) = - ϖ^{2} + \sum_{i} (ϖ s_{i})^{2} = ϖ^{2} (∣ s ∣^{2} - 1)$ by [L8]; by [L1] this value is $0$ , and $ϖ > 0$ by step 1.1, so $∣ s ∣^{2} = 1$ and $∣ s ∣ = 1$ .

2.2step 1.1step 1.2L1L6

Clause (d). Step 1.2 and $k_{i} = ϖ s_{i}$ , $k_{0} = - ϖ$ give $k^{♯} = - k_{0} e_{0} + k_{1} e_{1} + k_{2} e_{2} + k_{3} e_{3} = ϖ (e_{0} + s_{1} e_{1} + s_{2} e_{2} + s_{3} e_{3})$ by [L6]; the coefficient of $e_{0}$ is $ϖ > 0$ and the coordinates are $ϖ (1, s_{1}, s_{2}, s_{3})$ , so $k^{♯} \neq 0$ ; [L1] gives that $k^{♯}$ is future null and $k (k^{♯}) = η (k^{♯}, k^{♯}) = 0$ .

3.1step 1.1step 1.2step 1.3step 2.1step 2.2L2∎

Clause (f). By definition $ϖ = - k (e_{0})$ and $s_{i} = k (e_{i}) / ϖ$ are determined by $k$ and the frame (with $ϖ > 0$ by step 1.1), so the pair is unique for $k$ ; conversely, if two covectors have the same frame data, they take the same values on each $e_{a}$ , hence agree on all of $V$ by linearity and [L2]. Clause (c) exhibits the data of every future null wave covector, clause (e) shows every admissible pair arises from one, and steps 2.1 and 2.2 record $∣ s ∣ = 1$ and the raised vector; this proves (a)-(f). No choice principle was used.

LemmaStatement: AI-adaptedProof: AI-adaptedOpen item page →

Boost transformation of a future null wave covector and of its frame data

Statement

Let $(A, V, η, C^{+})$ be the oriented time-oriented affine Minkowski space, let $x$ and $x^{'}$ be inertial charts whose transition is $x^{'} = B (β) x + b$ for some $β \in R^{3}$ with $∣ β ∣ < 1$ and some $b \in R^{4}$ , where $B (β)$ is the passive boost of The passive Lorentz boost with parameter beta and $γ : = (1 - ∣ β ∣^{2})^{- 1 / 2}$ , and let $k$ be a future null wave covector with frame- $x$ data $(ϖ, s)$ as in Frame data of a future null wave covector: the unique pair $(ϖ, s)$ with $∣ s ∣ = 1$ , so that $k$ has components $(k_{0}, k_{1}, k_{2}, k_{3}) = (- ϖ, ϖ s_{1}, ϖ s_{2}, ϖ s_{3})$ in $x$ . Then:

(i) the components of the same covector $k$ in $x^{'}$ are $k_{a}^{'} = (B (- β))^{b}_{a} k_{b}$ , that is

$k_{0}^{'} = γ (k_{0} + β \cdot k_{v e c}), k_{v e c}^{'} = k_{v e c} + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot k_{v e c}) β + γ β k_{0}$

for $β \neq 0$ (and $k^{'} = k$ for $β = 0$ ), where $k_{v e c} : = (k_{1}, k_{2}, k_{3})$ ;

(ii) with $ϖ^{'} : = - k_{0}^{'}$ and $s_{i}^{'} : = k_{i}^{'} / ϖ^{'}$ the frame- $x^{'}$ data of $k$ is

$ϖ^{'} = γ (1 - β \cdot s) ϖ > 0, s^{'} = \frac{s + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot s) β - γ β}{γ (1 - β \cdot s)}$

for $β \neq 0$ (and $ϖ^{'} = ϖ$ , $s^{'} = s$ for $β = 0$ ); moreover $∣ s^{'} ∣ = 1$ , so $k_{a}^{'} = (- ϖ^{'}, ϖ^{'} s_{1}^{'}, ϖ^{'} s_{2}^{'}, ϖ^{'} s_{3}^{'})$ in $x^{'}$ ;

(iii) in the axis case $β = b e_{1}$ with $b \in (- 1, 1)$ : $s_{1}^{'} = (s_{1} - b) / (1 - b s_{1})$ , and $s_{2}^{'} = s_{2} / (γ (1 - b s_{1}))$ , $s_{3}^{'} = s_{3} / (γ (1 - b s_{1}))$ ;

(iv) $β \cdot s^{'} = (β \cdot s - ∣ β ∣^{2}) / (1 - β \cdot s)$ ; in particular $β \cdot s^{'} = 0$ if and only if $β \cdot s = ∣ β ∣^{2}$ , and $β \cdot s^{'} = - ∣ β ∣^{2}$ if and only if $β \cdot s = 0$ ;

(v) applying the transformation with $β$ replaced by $- β$ returns the original data $(ϖ, s)$ , since $B (- β)$ is the inverse of $B (β)$ .

The statement is pure algebra of $η$ and the boost; no choice principle is used.

Facts & Assumptions

Given: Inertial charts $x, x^{'}$ with $x^{'} = B (β) x + b$ , $β \in R^{3}$ , $∣ β ∣ < 1$ , $b \in R^{4}$ , $γ = (1 - ∣ β ∣^{2})^{- 1 / 2}$ , and a future null wave covector $k$ with frame- $x$ data $(ϖ, s)$ .

[L1]

$B (β)$ has matrix entries in the frame basis $B^{0}_{0} = γ$ , $B^{0}_{i} = B^{i}_{0} = - γ β_{i}$ , $B^{i}_{j} = δ_{j}^{i} + \frac{γ - 1}{∣ β ∣^{2}} β_{i} β_{j}$ for $i, j = 1, 2, 3$ and $β \neq 0$ , while $B (0) = id$ ; $γ \geq 1$ with equality exactly when $β = 0$ (The passive Lorentz boost with parameter beta).

[L2]

$B (β)$ is a proper orthochronous Lorentz map with $B (- β) = B (β)^{- 1}$ , and the transition $x^{'} = B (β) x + b$ of inertial charts has proper orthochronous linear part (The passive boost is a proper orthochronous Lorentz map with inverse B(-beta), Inertial charts are related by proper orthochronous affine Lorentz maps, and every such map is a chart transition, Linear and affine Lorentz maps, and the Lorentz group).

[L3]

For a constant covector field $k$ on $A$ (of class $C^{\infty}$ , in particular $C^{1}$ ) the components in the two charts satisfy $k_{a}^{'} = (Λ^{- 1})^{b}_{a} k_{b}$ , where $Λ$ is the linear part of the transition; here $Λ = B (β)$ and $Λ^{- 1} = B (- β)$ (Transformation of tensor, covector, derivative and current components under affine Lorentz maps, clause (ii), C^k tensor fields on affine Minkowski space and their inertial components, Inertial frames and inertial charts of the affine Minkowski model).

[L4]

Frame data of a future null wave covector in any inertial frame: for the frame of $x^{'}$ , the numbers $ϖ^{'} : = - k (e_{0}^{'})$ and $s_{i}^{'} : = k (e_{i}^{'}) / ϖ^{'}$ satisfy $ϖ^{'} > 0$ , $∣ s^{'} ∣ = 1$ and $k_{a}^{'} = (- ϖ^{'}, ϖ^{'} s_{1}^{'}, ϖ^{'} s_{2}^{'}, ϖ^{'} s_{3}^{'})$ (Frame data of a future null wave covector: the unique pair $(ϖ, s)$ with $∣ s ∣ = 1$ , clauses (a)-(d)).

[L5]

In the frame of $x$ , $k_{a} = (- ϖ, ϖ s_{1}, ϖ s_{2}, ϖ s_{3})$ , $ϖ > 0$ and $∣ s ∣ = 1$ , with coordinates taken in the frame's orthonormal basis and the Euclidean scalar product $β \cdot k_{v e c} = \sum_{i} β_{i} k_{i}$ (Frame data of a future null wave covector: the unique pair $(ϖ, s)$ with $∣ s ∣ = 1$ , The Euclidean spatial structure and cross product of an inertial frame, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

[L6]

$∣ β \cdot s ∣ \leq ∣ β ∣ ∣ s ∣ = ∣ β ∣ < 1$ , so $1 - β \cdot s > 0$ (The Cauchy-Schwarz inequality for finite sums, The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ).

Proof

technique · direct

1.1L1L2L3L5

Clause (i). Regard $k$ as the constant covector field on $A$ ; by [L3] its primed components are $k_{a}^{'} = (B (- β))^{b}_{a} k_{b}$ . For $β \neq 0$ the matrix of $B (- β)$ has entries $(B (- β))^{0}_{0} = γ$ , $(B (- β))^{0}_{i} = γ β_{i}$ , $(B (- β))^{i}_{0} = γ β_{i}$ and $(B (- β))^{i}_{j} = δ_{j}^{i} + \frac{γ - 1}{∣ β ∣^{2}} β_{i} β_{j}$ by [L1]; therefore $k_{0}^{'} = γ k_{0} + γ \sum_{i} β_{i} k_{i} = γ (k_{0} + β \cdot k_{v e c})$ and $k_{i}^{'} = γ β_{i} k_{0} + k_{i} + \frac{γ - 1}{∣ β ∣^{2}} β_{i} (β \cdot k_{v e c})$ , which is the displayed vector identity. For $β = 0$ one has $B (0) = id$ by [L1], so $k^{'} = k$ .

2.1step 1.1L4L5L6

Clause (ii). By step 1.1 and [L5], $k_{0}^{'} = γ (k_{0} + β \cdot k_{v e c}) = γ (- ϖ + β \cdot ϖ s) = - γ (1 - β \cdot s) ϖ$ , hence $ϖ^{'} = - k_{0}^{'} = γ (1 - β \cdot s) ϖ$ , and this is positive because $γ \geq 1$ , $ϖ > 0$ and $1 - β \cdot s > 0$ by [L6]; this also agrees with $ϖ^{'} > 0$ asserted by [L4]. Dividing the vector component of step 1.1 by $ϖ^{'}$ gives $s_{i}^{'} = k_{i}^{'} / ϖ^{'} = [s_{i} + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot s) β_{i} - γ β_{i}] / [γ (1 - β \cdot s)]$ for $β \neq 0$ , which is the displayed $s^{'}$ . For $β = 0$ , $k^{'} = k$ gives $ϖ^{'} = ϖ$ and $s^{'} = s$ . The normalization $∣ s^{'} ∣ = 1$ and the component form $k_{a}^{'} = (- ϖ^{'}, ϖ^{'} s^{'})$ are clauses (a)-(d) of [L4] applied in the frame of $x^{'}$ .

3.1step 2.1

Clause (iii). Let $β = b e_{1}$ with $b \in (- 1, 1)$ and $γ = (1 - b^{2})^{- 1 / 2}$ . If $b \neq 0$ , substituting $β_{1} = b$ , $β_{2} = β_{3} = 0$ and $β \cdot s = b s_{1}$ into step 2.1 gives $s_{1}^{'} = [s_{1} + \frac{γ - 1}{b^{2}} (b s_{1}) b - γ b] / [γ (1 - b s_{1})] = (s_{1} - b) / (1 - b s_{1})$ , because $s_{1} + (γ - 1) s_{1} - γ b = γ (s_{1} - b)$ , and $s_{2}^{'} = s_{2} / [γ (1 - b s_{1})]$ , $s_{3}^{'} = s_{3} / [γ (1 - b s_{1})]$ . If $b = 0$ then $γ = 1$ and $s^{'} = s$ by step 2.1, which is the same as the displayed formulas at $b = 0$ .

3.2step 2.1L1L6

Clause (iv). For $β \neq 0$ , step 2.1 gives $β \cdot s^{'} = [β \cdot s + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot s) (β \cdot β) - γ ∣ β ∣^{2}] / [γ (1 - β \cdot s)] = [β \cdot s + (γ - 1) (β \cdot s) - γ ∣ β ∣^{2}] / [γ (1 - β \cdot s)] = [γ (β \cdot s) - γ ∣ β ∣^{2}] / [γ (1 - β \cdot s)] = (β \cdot s - ∣ β ∣^{2}) / (1 - β \cdot s)$ ; for $β = 0$ both sides are $0$ , so the identity holds always. Since $1 - β \cdot s > 0$ by [L6], $β \cdot s^{'} = 0$ holds exactly when $β \cdot s = ∣ β ∣^{2}$ , and $β \cdot s^{'} = - ∣ β ∣^{2}$ holds exactly when $β \cdot s - ∣ β ∣^{2} = - ∣ β ∣^{2} (1 - β \cdot s)$ , that is $β \cdot s (1 - ∣ β ∣^{2}) = 0$ , which by $∣ β ∣ < 1$ is exactly $β \cdot s = 0$ .

4.1step 2.1step 3.2L2∎

Clause (v). The transition $x^{'} = B (β) x + b$ inverts to $x = B (- β) x^{'} + b^{'}$ with $b^{'} : = - B (- β) b$ , whose linear part $B (- β)$ is a proper orthochronous Lorentz map with $∣ - β ∣ = ∣ β ∣ < 1$ by [L2]; applying step 2.1 to the chart pair $(x^{'}, x)$ with parameter $- β$ computes the frame- $x$ data of $k$ from its frame- $x^{'}$ data, and that frame- $x$ data is $(ϖ, s)$ by hypothesis. Directly, $ϖ^{''} = γ (1 - (- β) \cdot s^{'}) ϖ^{'} = γ (1 + β \cdot s^{'}) ϖ^{'}$ and step 3.2 gives $1 + β \cdot s^{'} = (1 - β \cdot s + β \cdot s - ∣ β ∣^{2}) / (1 - β \cdot s) = (1 - ∣ β ∣^{2}) / (1 - β \cdot s)$ , so $ϖ^{''} = γ \cdot \frac{1 - ∣ β ∣^{2}}{1 - β \cdot s} \cdot γ (1 - β \cdot s) ϖ = γ^{2} (1 - ∣ β ∣^{2}) ϖ = ϖ$ ; the vector part of the same instance returns a unit vector $s^{''}$ with $k$ 's frame- $x$ data equal to $(ϖ^{''}, s^{''})$ , and by the uniqueness of frame data in [L4] applied to the frame of $x$ , $(ϖ^{''}, s^{''}) = (ϖ, s)$ , so $s^{''} = s$ . This proves (i)-(v); the argument is pure algebra of $η$ and the boost, and no choice principle was used.

LemmaStatement: AI-adaptedProof: AI-adaptedOpen item page →

The phase rate along a worldline is the wave covector evaluated on the four-velocity

Statement

Let $θ$ be an affine phase function with wave covector $k$ (Affine phase functions and wave covectors on affine Minkowski space). Then:

(a) for every $C^{1}$ curve $γ : I \to A$ in the sense of Affine phase functions and wave covectors on affine Minkowski space, clause (b), one has $(θ \circ γ)^{'} (s) = k (γ^{'} (s))$ for all $s \in I$ ;

(b) if $x : I \to A$ is a future timelike worldline (Curves, regular causal curves and future timelike worldlines in affine Minkowski space) with proper-time function $τ$ (Proper time along a future timelike worldline) and four-velocity $U = d x / d τ$ (Four-velocity and four-acceleration of a future timelike worldline), then $d (θ \circ x) / d τ = k (U)$ along the worldline, the derivative being taken in the proper-time parametrization, whose inverse exists by The proper-time function is a strictly increasing C^1 parametrization with C^1 inverse;

(c) if $k$ is moreover a future null wave covector, then $k (U) < 0$ at every point, so $θ$ is strictly decreasing in proper time along every future timelike worldline; the positive number $- k (U)$ is the quantity given physical meaning in def-sr-null-wave-covector-and-observer-frequency;

(d) if $k$ is a future null wave covector and $x$ is the straight worldline of an inertial observer, so that $U = c n$ for a future unit timelike vector $n$ with $η (n, n) = - 1$ , then $k (U) = c k (n)$ and $- k (U) = - c k (n) > 0$ ; conversely every future timelike worldline has $η (U, U) = - c^{2}$ (Norms of four-velocity and four-acceleration, and the observer rest-space decomposition).

No choice principle is used.

Facts & Assumptions

Given: An affine phase function $θ$ with wave covector $k$ on the affine Minkowski space, and a $C^{1}$ curve $γ : I \to A$ .

[L1]

$θ (p) - θ (q) = k (p - q)$ for all $p, q \in A$ , and for every $C^{1}$ curve $γ : I \to A$ one has $(θ \circ γ)^{'} (s) = k (γ^{'} (s))$ for all $s \in I$ (Affine phase functions and wave covectors on affine Minkowski space, clauses (a) and (b)).

[L2]

A future timelike worldline $x : I \to A$ is a $C^{1}$ curve whose tangent $x^{'} (s)$ is future timelike for every $s$ , and the parametrization is part of the curve (Curves, regular causal curves and future timelike worldlines in affine Minkowski space).

[L3]

The proper-time function $τ$ of a future timelike worldline is $C^{1}$ and strictly increasing with $τ^{'} (s) = c^{- 1} \sqrt{- η (x^{'} (s), x^{'} (s))} > 0$ ; its inverse $ρ : J \to I$ is $C^{1}$ with $ρ^{'} (τ (s)) = 1 / τ^{'} (s)$ , and $y : = x \circ ρ$ is a $C^{1}$ future timelike worldline with $y^{'} (τ (s)) = x^{'} (s) / τ^{'} (s)$ (Proper time along a future timelike worldline, The proper-time function is a strictly increasing C^1 parametrization with C^1 inverse).

[L4]

The four-velocity is $U (s) = x^{'} (s) / τ^{'} (s) = c x^{'} (s) / \sqrt{- η (x^{'} (s), x^{'} (s))}$ , it is future timelike, and $η (U (s), U (s)) = - c^{2}$ (Four-velocity and four-acceleration of a future timelike worldline, Norms of four-velocity and four-acceleration, and the observer rest-space decomposition, clause (a)).

[L5]

A future null wave covector has $k^{♯}$ nonzero future causal, and for a future timelike vector $n$ and a nonzero future causal vector $v$ one has $η (n, v) < 0$ ; moreover $k (w) = η (k^{♯}, w)$ for every $w$ (Affine phase functions and wave covectors on affine Minkowski space, A future timelike vector pairs negatively with every nonzero future causal vector, clause (a)).

[L6]

The one-variable chain rule and the definition of the derivative (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , 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).

[L7]

A real function continuous on $[a, b]$ and differentiable on $(a, b)$ , with $a < b$ , has $f (b) - f (a) = f^{'} (r) (b - a)$ for some $r \in (a, b)$ (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

Proof

technique · direct

1.1L1

Clause (a). This is exactly the chain-rule identity recorded in [L1] for $C^{1}$ curves: $(θ \circ γ)^{'} (s) = k (γ^{'} (s))$ .

2.1step 1.1L1L3L4L6

Clause (b). By [L3] the inverse $ρ : J \to I$ of $τ$ exists and is $C^{1}$ , and the proper-time parametrized worldline $y : = x \circ ρ$ satisfies $y (τ (s)) = x (s)$ and $y^{'} (τ (s)) = x^{'} (s) / τ^{'} (s) = U (s)$ for every $s \in I$ , the last equality by [L4]. The real function $θ \circ x$ on $I$ equals $(θ \circ y) \circ τ$ ; differentiating at $s$ with the chain rule [L6] gives $(θ \circ x)^{'} (s) = (θ \circ y)^{'} (τ (s)) τ^{'} (s)$ , and clause (a), applied to the $C^{1}$ curve $y$ [L1, L3], gives $(θ \circ y)^{'} (τ (s)) = k (y^{'} (τ (s))) = k (U (s))$ . Hence $d (θ \circ x) / d τ : = \frac{(θ \circ x)^{'} (s)}{τ^{'} (s)} = (θ \circ y)^{'} (τ (s)) = k (U (s))$ , since $τ^{'} (s) \neq 0$ [L3].

3.1step 2.1L2L3L4L5L7

Clause (c). For the worldline of [L2], if $k$ is future null, [L4, L5] give $k (U (s)) = η (U (s), k^{♯}) < 0$ for every $s \in I$ . By step 2.1 the $C^{1}$ function $f : = θ \circ y : J \to R$ has $f^{'} (τ (s)) = k (U (s)) < 0$ . For any $a < b$ in the interval $J$ , its restriction to $[a, b]$ is continuous and differentiable on $(a, b)$ ; [L7] gives $f (b) - f (a) = f^{'} (r) (b - a) < 0$ for some $r \in (a, b)$ . Thus the phase is strictly decreasing in proper time, including comparisons with endpoints, and $- k (U) > 0$ .

4.1step 1.1step 2.1step 3.1L4L5∎

Clause (d). If $U = c n$ with $n$ future unit timelike, then $k (U) = c k (n)$ by linearity of $k$ , and $k (n) = η (k^{♯}, n) = η (n, k^{♯}) < 0$ by [L5] applied to the future timelike vector $n$ and the nonzero future causal vector $k^{♯}$ ; hence $- k (U) = - c k (n) > 0$ . The converse claim is clause (a) of [L4], valid for every future timelike worldline. Together with steps 1.1, 2.1 and 3.1 this proves (a)-(d); no choice principle was used.

DefinitionDefinition: AI-adaptedProof: AI-adaptedOpen item page →

Null wave covectors, frame frequency data and the observer frequency of an ideal plane wave

Physical scope

Ideal wave vocabulary in flat classical special-relativistic spacetime: the angular frequency, linear frequency, wave vector, wavelength and propagation direction attached to a future null wave covector in an inertial frame, and the observer-frequency sign convention omega_n = -c k(n) = -k(U_o) for an ideal observer. Conditional on the model's SI conventions; excludes quantum photon and energy identifications, media and dispersion, amplitude and intensity, sources and detectors, real apparatus, and every measurement or empirical claim.

Definition

Adopt the SI coordinate and unit conventions of SI units and coordinate conventions of the special-relativity framework: in every inertial chart $x^{0} = c t$ with $c > 0$ in metres per second and spatial coordinates in metres, so $c$ is the model's conversion constant. Let $k$ be a future null wave covector and $θ$ its affine phase (Affine phase functions and wave covectors on affine Minkowski space). Take $θ$ dimensionless; its covector components then have unit $m^{- 1}$ .

Angular convention. Here angles use radian arc length on the unit circle. An explicit construction, also fixing $π$ , is $a (t) : = 2 \int_{0}^{t} (1 + r^{2})^{- 1} d r$ for $0 \leq t \leq 1$ , and $π : = 2 a (1)$ . These are finite Riemann integrals (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ): the integrand is continuous with positive denominator by Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function and integrable by A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion. By The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive, $a^{'} (t) = 2 / (1 + t^{2}) > 0$ ; The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ makes $a$ strictly increasing, and Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ makes it a bijection onto $[0, π / 2]$ . This is the arc-length parameter of the quarter-circle $q (t) = ((1 - t^{2}) / (1 + t^{2}), 2 t / (1 + t^{2}))$ : the sum, product and quotient rules of 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$ give $q^{'} (t) = (- 4 t, 2 (1 - t^{2})) / (1 + t^{2})^{2}$ , hence $∣ q^{'} (t) ∣ = 2 / (1 + t^{2})$ , and $∣ q (t) ∣ = 1$ .

For $α \in [0, π / 2]$ , let $t$ be the unique value with $a (t) = α$ and define $\cos α : = (1 - t^{2}) / (1 + t^{2})$ and $\sin α : = 2 t / (1 + t^{2})$ ; for $α \in [π / 2, π]$ use the unique $t$ with $a (t) = π - α$ and define $\cos α : = - (1 - t^{2}) / (1 + t^{2})$ and $\sin α : = 2 t / (1 + t^{2})$ . The definitions agree at $π / 2$ . The rational function $(1 - t^{2}) / (1 + t^{2})$ decreases continuously from $1$ to $0$ , since its difference at $v > u \geq 0$ is $- 2 (v^{2} - u^{2}) / [(1 + v^{2}) (1 + u^{2})] < 0$ . Thus cosine is a strictly decreasing bijection $[0, π] \to [- 1, 1]$ ; write $\arccos$ for its inverse. For spatial coordinate vectors $v, w \in R^{3}$ in one named inertial frame, write $v \cdot w : = \sum_{i = 1}^{3} v_{i} w_{i}$ and $∣ v ∣ : = \sqrt{\sum_{i = 1}^{3} v_{i}^{2}}$ . If $v, w$ are nonzero, their norms are positive and their angle is $\arccos ((v \cdot w) / (∣ v ∣ ∣ w ∣))$ : The Cauchy-Schwarz inequality for finite sums, applied to the three real coordinate entries, gives $∣ v \cdot w ∣ \leq ∣ v ∣ ∣ w ∣$ , so division by $∣ v ∣ ∣ w ∣ > 0$ puts the argument in $[- 1, 1]$ . For unit vectors it is $\arccos (v \cdot w)$ . These formulas give $\sin α \geq 0$ and $\sin^{2} α + \cos^{2} α = 1$ on $[0, π]$ and fix a full turn as $2 π$ .

(a) Frame data as wave data. In the inertial chart of a frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ (Inertial frames and inertial charts of the affine Minkowski model) let $(ϖ, s)$ be the frame data of $k$ given by Frame data of a future null wave covector: the unique pair $(ϖ, s)$ with $∣ s ∣ = 1$ , so $ϖ = - k (e_{0}) > 0$ and $∣ s ∣ = 1$ . Define the angular frequency $ω : = c ϖ$ (unit $s^{- 1}$ ), the linear frequency $ν : = ω / (2 π)$ (unit $s^{- 1}$ , hertz), the wave vector $κ : = (ω / c) s$ (unit $m^{- 1}$ , with $∣ κ ∣ = ω / c$ ), the wavelength $λ : = 2 π / ∣ κ ∣ = 2 π c / ω = c / ν$ (unit $m$ ), and the propagation direction $s$ (dimensionless). In these conventions the phase is $θ (p) = - ω t + κ \cdot x_{v e c} (p) + c o n s t$ with $t : = x^{0} (p) / c$ the coordinate time in seconds, so the components of $k$ in the chart are

$k_{a} = (- ω / c, (ω / c) s_{1}, (ω / c) s_{2}, (ω / c) s_{3}) .$

(b) Observer frequency. For an ideal observer whose four-velocity is $U_{o} = c n$ with $n \in V$ future unit timelike, $η (n, n) = - 1$ (Four-velocity and four-acceleration of a future timelike worldline, Norms of four-velocity and four-acceleration, and the observer rest-space decomposition), define the observer angular frequency of the wave as

$ω_{n} : = - c k (n) = - k (U_{o}) (unit s^{- 1}),$

and the observer linear frequency as $ω_{n} / (2 π)$ . By The phase rate along a worldline is the wave covector evaluated on the four-velocity this is minus the rate of change of the phase with respect to the observer's own proper time, and the sign convention makes it positive.

(c) Well-definedness. $ϖ = - k (e_{0}) > 0$ and $∣ s ∣ = 1$ in every inertial frame, hence $ω > 0$ and $λ > 0$ are well defined and independent of the choices made in their computation (frame-data lemma); $ω_{n} > 0$ for every future unit timelike $n$ and every future null wave covector $k$ (A future timelike vector pairs negatively with every nonzero future causal vector, The metric pairing is a linear bijection to the dual, and the raised covector in an orthonormal frame), so every ideal observer reads a positive angular frequency, and $ω_{n}$ depends only on $k$ and the observer vector $n$ . The classification of $k$ as future null is the one of Timelike, null, spacelike and causal vectors of a Lorentz vector space and Time orientation, future and past timelike/null/causal vectors, and the closed cones.

(d) Scope. This item fixes definitions, units and sign conventions only. It does not assert that any physical light is described by such a phase; that identification is adopted in post-sr-ideal-plane-wave-model. It contains no quantum identification of energy with $ℏ ω$ , no amplitude or intensity content, no medium or dispersion model, no source or detector model, and no measurement or empirical claim. No choice principle is used.

PostulateStatement: AI-adaptedProof: Not applicableOpen item page →

Adopted ideal plane-wave and frequency-reading model

Physical scope

Ideal monochromatic vacuum plane waves and ideal observers in the flat classical special-relativity model: the phase model with future null wave covector, the identification of wave fronts and ideal rays, and the phase-per-proper-time frequency reading by an ideal observer. Adopted assumptions, not deductions and not empirical findings; excludes quantum, medium, dispersion, source, detector, intensity, polarization, gravity and real-apparatus effects; empirical tests are reserved to the framework's experimental work.

Postulate

Adopt as physical assumptions of this framework, extending Adopted ideal-clock and ideal-vacuum-light interpretation (ideal vacuum light rays are exactly the future null straight lines, with coordinate speed $c$ in every inertial chart) and Adopted inertial covariance of the model equations (the affine Minkowski model, with the model's equations covariant under proper orthochronous affine Lorentz maps):

(i) Ideal plane wave. An ideal monochromatic light wave in vacuum is modeled, in any inertial chart, by a dimensionless affine phase $θ$ with future null wave covector $k$ (Affine phase functions and wave covectors on affine Minkowski space, Frame data of a future null wave covector: the unique pair $(ϖ, s)$ with $∣ s ∣ = 1$ ): the level sets of $θ$ are the wave fronts, and the complete ray trajectories of this wave are the constant-phase lines $λ \mapsto p + λ k^{♯}$ for $λ \in R$ , whose tangents are future null. Their future portions from $p$ have images $p + R_{\geq 0} k^{♯}$ . The complete trajectories are ideal light rays in the sense of Adopted ideal-clock and ideal-vacuum-light interpretation; the portions are half-lines. The model is one ideal plane wave: constant wave covector, no medium, no dispersion, no absorption, no modulation or envelope, no boundary or source model, no intensity or polarization model.

(ii) Frequency reading. An ideal observer of the model with four-velocity $U_{o} = c n$ ( $n$ future unit timelike) that receives this wave reads the angular frequency $ω_{n} : = - c k (n) = - k (U_{o})$ and the linear frequency $ω_{n} / (2 π)$ of Null wave covectors, frame frequency data and the observer frequency of an ideal plane wave, that is, minus the rate of change of the phase with respect to the observer's own proper time with the sign convention that this number is positive (The phase rate along a worldline is the wave covector evaluated on the four-velocity, A future timelike vector pairs negatively with every nonzero future causal vector). The reading is attached to the observer's worldline at the event of reception.

(iii) Frequency comparisons. Comparing the frequency of one wave between two ideal observers or between two inertial descriptions means comparing $ω_{n}$ at specified reception events, or the frame data $(ω, s)$ of the same phase function in specified inertial charts; this postulate asserts no Doppler or aberration formula, and comparing events requires propagating the phase along the specified observer worldlines.

(iv) Scope and exclusions. These are adopted idealizations, not deductions from experiment and not claims about nature. No quantum photon model and no identification of energy with $ℏ ω$ is made; no claim is made that real light, real clocks, real receivers or real sources are exactly described; dispersive, absorbing, nonlinear or modulated media, finite line width, intensity, polarization, source and detector physics, gravitation, quantum effects and accelerated-observer reception are outside the model. Empirical tests of the model belong to the framework's experimental work and are not asserted here.

No choice principle is used in this formulation; the postulate is an adopted assumption of the model, not a proved assertion.

Physics theoremStatement: AI-adaptedProof: AI-adaptedOpen item page →

Doppler shift and aberration for an ideal plane wave between inertial descriptions

Physical scope

Conditional Doppler-shift and aberration predictions of the ideal plane-wave model of flat classical special-relativistic spacetime, for inertial descriptions related by a passive boost and for ideal observers with subluminal coordinate velocity. Excludes quantum photons, media and dispersion, intensity and polarization, real sources and detectors, accelerating observers, gravitation, and every measurement, statistical or empirical claim; the idealizations of the adopted postulates travel to all consumers.

Statement

Adopt Adopted inertial covariance of the model equations, Adopted ideal-clock and ideal-vacuum-light interpretation and Adopted ideal plane-wave and frequency-reading model, and the conventions of SI units and coordinate conventions of the special-relativity framework. Let $x$ and $x^{'}$ be inertial charts whose transition is $x^{'} = B (β) x + b$ with $β \in R^{3}$ , $∣ β ∣ < 1$ , $b \in R^{4}$ and $B (β)$ the passive boost of The passive Lorentz boost with parameter beta; write $γ : = (1 - ∣ β ∣^{2})^{- 1 / 2}$ and $β_{h a t} : = β / ∣ β ∣$ for $β \neq 0$ , so that the frame $x^{'}$ moves with velocity $v = c β$ relative to the frame $x$ in the direction $β_{h a t}$ (step 1.1 records this). Let the ideal wave of the model have phase $θ$ with future null wave covector $k$ and frame- $x$ data $(ω, s)$ in the sense of Null wave covectors, frame frequency data and the observer frequency of an ideal plane wave: $ω > 0$ , $s \in R^{3}$ with $∣ s ∣ = 1$ and $k_{a} = (- ω / c, (ω / c) s_{1}, (ω / c) s_{2}, (ω / c) s_{3})$ in $x$ . Then, conditionally on the adopted model:

(i) Frame data in $x^{'}$ . The data of the same covector $k$ in $x^{'}$ is $(ω^{'}, s^{'})$ with

$ω^{'} = γ (1 - β \cdot s) ω > 0, s^{'} = \frac{s + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot s) β - γ β}{γ (1 - β \cdot s)}$

for $β \neq 0$ (and $ω^{'} = ω$ , $s^{'} = s$ for $β = 0$ ), so $∣ s^{'} ∣ = 1$ and $k_{a}^{'} = (- ω^{'} / c, (ω^{'} / c) s_{1}^{'}, (ω^{'} / c) s_{2}^{'}, (ω^{'} / c) s_{3}^{'})$ in $x^{'}$ . In the axis case $β = b e_{1}$ with $b \in (- 1, 1)$ : $s_{1}^{'} = (s_{1} - b) / (1 - b s_{1})$ and $(s_{2}^{'}, s_{3}^{'}) = (s_{2}, s_{3}) / [γ (1 - b s_{1})]$ .

(ii) Reading and frequency ratios. The rest observers of $x$ and $x^{'}$ (four-velocities $c e_{0}$ and $c e_{0}^{'}$ ) read angular frequencies $ω = - c k (e_{0})$ and $ω^{'} = - c k (e_{0}^{'})$ ; the linear frequencies and wavelengths of the two descriptions satisfy $ν^{'} = γ (1 - β \cdot s) ν$ and $λ^{'} = λ / [γ (1 - β \cdot s)]$ . More generally, an ideal inertial observer whose constant coordinate velocity in $x$ is $w$ (a vector of the frame's spatial three-space with $∣ w ∣ < c$ ) reads

$ω_{o} = γ_{w} (1 - \frac{w \cdot s}{c}) ω, γ_{w} : = (1 - \frac{∣ w ∣^{2}}{c^{2}})^{- 1 / 2};$

equivalently $ω_{o} = γ_{w} (1 - β_{w} \cdot s) ω$ with $β_{w} : = w / c$ .

(iii) Longitudinal cases. For $β \neq 0$ , if $s = β_{h a t}$ then $ω^{'} = ω \sqrt{(1 - ∣ β ∣) / (1 + ∣ β ∣)} < ω$ , $ν^{'} = ν \sqrt{(1 - ∣ β ∣) / (1 + ∣ β ∣)}$ and $λ^{'} = λ \sqrt{(1 + ∣ β ∣) / (1 - ∣ β ∣)}$ : the observer moving in the direction of propagation (in the interpretation of a source at rest in $x$ located behind the observer) reads a red-shifted frequency and lengthened wavelength. If $s = - β_{h a t}$ then $ω^{'} = ω \sqrt{(1 + ∣ β ∣) / (1 - ∣ β ∣)} > ω$ and $λ^{'} = λ \sqrt{(1 - ∣ β ∣) / (1 + ∣ β ∣)}$ : blue shift for an observer moving opposite to the propagation direction (toward such a source). At $β = 0$ every direction has $ω^{'} = ω$ , $ν^{'} = ν$ and $λ^{'} = λ$ ; no normalized boost axis is defined.

(iv) Transverse protocols. If $β \cdot s = 0$ (propagation direction perpendicular to the relative velocity in the frame $x$ ) then $ω^{'} = γ ω$ ; this is greater than $ω$ when $β \neq 0$ and equals $ω$ when $β = 0$ . If $β \cdot s = ∣ β ∣^{2}$ , equivalently $s^{'} \cdot β_{h a t} = 0$ for $β \neq 0$ (propagation direction perpendicular to the relative velocity in the frame $x^{'}$ ), then $ω^{'} = ω / γ$ ; this is less than $ω$ when $β \neq 0$ and equals $ω$ when $β = 0$ . Both configurations are called transverse Doppler configurations in the literature, and the two factors differ for $β \neq 0$ : the direction and size of the shift are not determined by the word "transverse" without specifying the frame in which transversality holds.

(v) Aberration. For $β \neq 0$ , define $θ_{x} : = \arccos (β_{h a t} \cdot s)$ and $θ_{x^{'}} : = \arccos (β_{h a t} \cdot s^{'})$ in $[0, π]$ , using the angular convention of Null wave covectors, frame frequency data and the observer frequency of an ideal plane wave. The primed scalar product uses the same numerical axis components in the primed frame's spatial coordinates; the two rest spaces themselves are distinct. Then

$\cos θ_{x^{'}} = \frac{\cos θ_{x} - ∣ β ∣}{1 - ∣ β ∣ \cos θ_{x}};$

the map $u \mapsto (u - ∣ β ∣) / (1 - ∣ β ∣ u)$ is a strictly increasing bijection of $[- 1, 1]$ onto itself, and in particular $\cos θ_{x} = 0$ gives $\cos θ_{x^{'}} = - ∣ β ∣$ .

(vi) Scope and protocol. All clauses concern one ideal plane wave and ideal observers, and frequencies are compared through the phase model at specified reception events; the results are conditional on the adopted postulates (ideal plane wave, ideal clocks, inertial covariance, flat classical spacetime) and are not empirical claims about nature, sources or apparatus. They exclude media and dispersion, modulation and signal speeds, intensity and polarization, real line widths, accelerating observers, gravitation and quantum effects; no statistical or measurement statement is made. If $β = 0$ the transition is the pure translation $x^{'} = x + b$ : the inertial axes and wave-covector frame data agree, with $ω^{'} = ω$ and $s^{'} = s$ , while the affine phase constant is transformed as in the covector and phase law.

Facts & Assumptions

Given: Inertial charts $x, x^{'}$ with $x^{'} = B (β) x + b$ , $β \in R^{3}$ , $∣ β ∣ < 1$ , $b \in R^{4}$ ; $γ = (1 - ∣ β ∣^{2})^{- 1 / 2}$ ; and an ideal plane wave with phase $θ$ , future null wave covector $k$ and frame- $x$ data $(ω, s)$ .

[A1]

Adopted ideal plane-wave model: the level sets of $θ$ are the wave fronts, the complete ray trajectories are the constant-phase future-directed null lines $λ \mapsto p + λ k^{♯}$ for $λ \in R$ , their future portions have images $p + R_{\geq 0} k^{♯}$ , and an ideal observer with four-velocity $U_{o} = c n$ reads the angular frequency $- c k (n) = - k (U_{o})$ at the reception event (Adopted ideal plane-wave and frequency-reading model).

[A2]

Adopted ideal light: ideal vacuum light rays are exactly the future null straight lines, with coordinate speed $c$ in every inertial chart, and real clocks and light are not claimed to be exactly ideal (Adopted ideal-clock and ideal-vacuum-light interpretation).

[A3]

Adopted inertial covariance: the inertial changes of description of the model are the affine maps with proper orthochronous Lorentz linear part, and covariance is asserted only for the specified model equations (Adopted inertial covariance of the model equations).

[L1]

With the SI conventions $x^{0} = c t$ , the frame data $(ϖ, s)$ of $k$ in a frame and the wave data are related by $ϖ = ω / c$ , $∣ s ∣ = 1$ , $ω > 0$ , $k_{a} = (- ω / c, (ω / c) s_{1}, (ω / c) s_{2}, (ω / c) s_{3})$ , $ν = ω / (2 π)$ , $λ = c / ν$ ; and an ideal observer with four-velocity $U_{o} = c n$ ( $n$ future unit timelike) reads $ω_{n} = - c k (n) = - k (U_{o}) > 0$ , which is minus the phase rate along the observer's worldline (Null wave covectors, frame frequency data and the observer frequency of an ideal plane wave, SI units and coordinate conventions of the special-relativity framework, Frame data of a future null wave covector: the unique pair $(ϖ, s)$ with $∣ s ∣ = 1$ , The phase rate along a worldline is the wave covector evaluated on the four-velocity, Affine phase functions and wave covectors on affine Minkowski space).

[L2]

Boost transformation of the frame data: for the chart pair of the Given, with $ϖ = ω / c$ and $β \neq 0$ , the frame- $x^{'}$ data $(ϖ^{'}, s^{'})$ satisfies $ϖ^{'} = γ (1 - β \cdot s) ϖ$ , $s^{'} = [s + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot s) β - γ β] / [γ (1 - β \cdot s)]$ , $∣ s^{'} ∣ = 1$ and $k_{a}^{'} = (- ϖ^{'}, ϖ^{'} s^{'})$ ; for $β = 0$ , $ϖ^{'} = ϖ$ , $s^{'} = s$ ; in the axis case $β = b e_{1}$ , $s_{1}^{'} = (s_{1} - b) / (1 - b s_{1})$ , $s_{2}^{'} = s_{2} / [γ (1 - b s_{1})]$ , $s_{3}^{'} = s_{3} / [γ (1 - b s_{1})]$ ; and $β \cdot s^{'} = (β \cdot s - ∣ β ∣^{2}) / (1 - β \cdot s)$ , with $β \cdot s^{'} = 0$ if and only if $β \cdot s = ∣ β ∣^{2}$ (Boost transformation of a future null wave covector and of its frame data).

[L3]

$γ \geq 1$ with equality exactly when $β = 0$ , $B (0) = id$ , and the matrix entries of $B (β)$ and $B (- β)$ are as displayed in The passive Lorentz boost with parameter beta; the transition $x^{'} = B (β) x + b$ of inertial charts has proper orthochronous linear part (Inertial charts are related by proper orthochronous affine Lorentz maps, and every such map is a chart transition), and $B (- β) = B (β)^{- 1}$ (Boost transformation of a future null wave covector and of its frame data, clause (v)).

[L4]

In an inertial frame the basis vectors satisfy $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)$ with $e_{0}$ future, so $e_{0}$ and $e_{0}^{'}$ are future unit timelike; the four-velocity of an observer at rest in a frame is $c$ times its first basis vector, and a point observer is a future unit timelike vector $n$ (Inertial frames and inertial charts of the affine Minkowski model, Four-velocity and four-acceleration of a future timelike worldline).

[L5]

Frame and component relations between the charts: the transition $x^{'} = Λ x + b$ has linear part $Λ = B (β)$ , the new frame's basis vectors satisfy $e_{a}^{'} = \sum_{b} (Λ^{- 1})^{b}_{a} e_{b}$ , and the components of a covector satisfy $k_{a}^{'} = (Λ^{- 1})^{b}_{a} k_{b}$ with $Λ^{- 1} = B (- β)$ ; in the chart of any inertial frame an affine phase with wave covector $k$ has the form $θ (p) = k_{a} x^{a} (p) + θ (o)$ (Inertial charts are related by proper orthochronous affine Lorentz maps, and every such map is a chart transition, Boost transformation of a future null wave covector and of its frame data, The passive Lorentz boost with parameter beta, Affine phase functions and wave covectors on affine Minkowski space).

[L6]

Relative velocity and coordinate form: for future unit timelike $n, u$ , with $γ_{r e l} : = - η (n, u)$ and $h (v) : = v + η (n, v) n$ , the vector $w : = c h (u) / γ_{r e l}$ lies in $n^{⊥}$ and is the velocity of the worldline with four-velocity $c u$ relative to the observer $n$ ; a worldline with coordinate velocity $w$ in an inertial chart, $∣ w ∣ < c$ , has four-velocity $U = γ_{w} (c, w_{v e c})$ with $γ_{w} = (1 - ∣ w ∣^{2} / c^{2})^{- 1 / 2}$ , so $n = U / c = γ_{w} (1, w / c)$ is future unit timelike (Norms of four-velocity and four-acceleration, and the observer rest-space decomposition, clauses (a), (c), (d), (e)).

[L7]

Each inertial frame has its own Euclidean spatial three-space. In all displayed direction formulas $β, s, w$ and $s^{'}$ are spatial coordinate triples; primed triples refer to the primed basis, while $β$ supplies the common numerical boost-axis components. Norms and scalar products of triples are Euclidean; in particular $s^{'} \cdot β_{h a t} = (β \cdot s^{'}) / ∣ β ∣$ for $β \neq 0$ (The Euclidean spatial structure and cross product of an inertial frame). Angles and the cosine inverse are defined in the angular convention of Null wave covectors, frame frequency data and the observer frequency of an ideal plane wave. The factor $1 - β \cdot s$ is positive because [L2] exhibits $ϖ^{'} = γ (1 - β \cdot s) ϖ$ with $ϖ, ϖ^{'}, γ > 0$ .

Proof

technique · direct

1.1L3L4L5L6

Setup, and the relative velocity of the frames. By [L1] the frame- $x$ data of $k$ is $(ϖ, s)$ with $ϖ = ω / c > 0$ . By the frame relation of [L5], $e_{0}^{'} = \sum_{b} (Λ^{- 1})^{b}_{0} e_{b}$ is the first column of $B (- β)$ , namely $(γ, γ β_{1}, γ β_{2}, γ β_{3})$ by [L3], so $e_{0}^{'} = γ (e_{0} + \sum_{i} β_{i} e_{i})$ . Then $η (e_{0}, e_{0}^{'}) = γ η (e_{0}, e_{0}) = - γ$ and $h (e_{0}^{'}) = e_{0}^{'} + η (e_{0}, e_{0}^{'}) e_{0} = γ e_{0} + γ \sum_{i} β_{i} e_{i} - γ e_{0} = γ \sum_{i} β_{i} e_{i}$ ; by [L6] with $n = e_{0}$ and $u = e_{0}^{'}$ , the velocity of the $x^{'}$ -rest observer relative to the $x$ -rest observer is $c h (e_{0}^{'}) / (- η (e_{0}, e_{0}^{'})) = c γ \sum_{i} β_{i} e_{i} / γ = c β$ , of magnitude $c ∣ β ∣$ in the direction $β_{h a t}$ when $β \neq 0$ .

2.1step 1.1L1L2L3L5L7

Clause (i). By the covector component law [L5] and [L3], $k_{a}^{'} = (B (- β))^{b}_{a} k_{b}$ ; with $k_{0} = - ω / c$ and $k_{i} = (ω / c) s_{i}$ from [L1] and the matrix entries of $B (- β)$ , this gives $k_{0}^{'} = γ (k_{0} + β \cdot k_{v e c}) = - γ (1 - β \cdot s) ω / c$ , with $1 - β \cdot s > 0$ by the positivity clause of [L2], and $k_{i}^{'} = k_{i} + γ β_{i} k_{0} + \frac{γ - 1}{∣ β ∣^{2}} β_{i} (β \cdot k_{v e c}) = \frac{ω}{c} [s_{i} - γ β_{i} + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot s) β_{i}]$ for $β \neq 0$ (and $k^{'} = k$ for $β = 0$ ). By the frame-data lemma [L2] the frame- $x^{'}$ data is $(ϖ^{'}, s^{'})$ with $ϖ^{'} = γ (1 - β \cdot s) ϖ = γ (1 - β \cdot s) ω / c$ , $s^{'} = [s + \frac{γ - 1}{∣ β ∣^{2}} (β \cdot s) β - γ β] / [γ (1 - β \cdot s)]$ , $∣ s^{'} ∣ = 1$ and $k_{a}^{'} = (- ϖ^{'}, ϖ^{'} s^{'})$ ; in wave data this is $ω^{'} = c ϖ^{'} = γ (1 - β \cdot s) ω > 0$ and the displayed $s^{'}$ , and the axis case is the axis clause of [L2].

3.1step 2.1L1L4L6

Clause (ii). By [L1] the rest observer of $x$ has four-velocity $c e_{0}$ and reads $ω_{e_{0}} = - c k (e_{0}) = c ϖ = ω$ , and the rest observer of $x^{'}$ has four-velocity $c e_{0}^{'}$ by [L4] and reads $ω_{e_{0}^{'}} = - c k (e_{0}^{'}) = c ϖ^{'} = ω^{'} = γ (1 - β \cdot s) ω$ by step 2.1, so $ν^{'} = ω^{'} / (2 π) = γ (1 - β \cdot s) ν$ and $λ^{'} = c / ν^{'} = λ / [γ (1 - β \cdot s)]$ by the relations $ν = ω / (2 π)$ , $λ = c / ν$ of [L1]. For the general observer, [L6] gives $U_{o} = γ_{w} (c, w_{v e c})$ , so $n = U_{o} / c = γ_{w} (1, w / c)$ is future unit timelike and, using linearity of $k$ and $k (e_{0}) = - ω / c$ , $k (e_{i}) = (ω / c) s_{i}$ [L1], $ω_{o} = - c k (n) = - c γ_{w} [k (e_{0}) + \sum_{i} (w_{i} / c) k (e_{i})] = γ_{w} ω (1 - (w \cdot s) / c)$ ; with $β_{w} = w / c$ this is $γ_{w} (1 - β_{w} \cdot s) ω$ .

3.2step 2.1L1L2L7

Clause (iii). Assume $β \neq 0$ . If $s = β_{h a t}$ then $β \cdot s = ∣ β ∣$ by [L7], so step 2.1 together with $ω = c ϖ$ and [L2] gives $ω^{'} = γ (1 - ∣ β ∣) ω$ , and since $0 \leq ∣ β ∣ < 1$ , $γ (1 - ∣ β ∣) = (1 - ∣ β ∣) / \sqrt{1 - ∣ β ∣^{2}} = \sqrt{(1 - ∣ β ∣) / (1 + ∣ β ∣)}$ , which is $< 1$ for $∣ β ∣ > 0$ and $= 1$ for $β = 0$ ; substituting $s = β_{h a t}$ in the formula of [L2] gives $s^{'} = β_{h a t}$ , so the propagation direction relative to the boost axis is unchanged. The wavelength and frequency ratios are $ν^{'} = ω^{'} / (2 π) = γ (1 - ∣ β ∣) ν$ and $λ^{'} = c / ν^{'} = λ / [γ (1 - ∣ β ∣)] = λ \sqrt{(1 + ∣ β ∣) / (1 - ∣ β ∣)}$ by $ν = ω / (2 π)$ , $λ = c / ν$ [L1] and $ω^{'} = γ (1 - ∣ β ∣) ω$ . If $s = - β_{h a t}$ the same computation with $- β_{h a t}$ gives $ω^{'} = γ (1 + ∣ β ∣) ω = ω \sqrt{(1 + ∣ β ∣) / (1 - ∣ β ∣)} > ω$ for $∣ β ∣ > 0$ , $s^{'} = - β_{h a t}$ and $λ^{'} = λ \sqrt{(1 - ∣ β ∣) / (1 + ∣ β ∣)}$ ; the source language in the statement is an interpretation of these factors, the model carrying no source.

3.3step 2.1L2L3L7

Clause (iv). If $β \cdot s = 0$ , step 2.1 gives $ω^{'} = γ ω$ , which is greater than $ω$ exactly when $γ > 1$ , that is exactly when $β \neq 0$ , and equals $ω$ when $β = 0$ , by [L3]. If $β \cdot s = ∣ β ∣^{2}$ , then by [L2] $β \cdot s^{'} = 0$ , and for $β \neq 0$ this is equivalent to $s^{'} \cdot β_{h a t} = (β \cdot s^{'}) / ∣ β ∣ = 0$ ; conversely $s^{'} \cdot β_{h a t} = 0$ with $β \neq 0$ gives $β \cdot s^{'} = 0$ and hence $β \cdot s = ∣ β ∣^{2}$ by [L2]. With $β \cdot s = ∣ β ∣^{2}$ step 2.1 gives $ω^{'} = γ (1 - ∣ β ∣^{2}) ω = ω / γ$ , which is less than $ω$ when $β \neq 0$ and equals $ω$ when $β = 0$ .

3.4step 2.1L2L7algebra

Clause (v). For $β \neq 0$ put $u : = \cos θ_{x} = β_{h a t} \cdot s = (β \cdot s) / ∣ β ∣$ and $u^{'} : = \cos θ_{x^{'}} = β_{h a t} \cdot s^{'} = (β \cdot s^{'}) / ∣ β ∣$ by [L7]; by the formula for $s^{'}$ of step 2.1, equivalently by [L2], $u^{'} = (β \cdot s - ∣ β ∣^{2}) / [∣ β ∣ (1 - β \cdot s)] = (u - ∣ β ∣) / (1 - ∣ β ∣ u)$ . Write $b : = ∣ β ∣$ and $f (u) : = (u - b) / (1 - b u)$ ; since $0 \leq b < 1$ one has $1 - b u \geq 1 - b > 0$ for every $u \in [- 1, 1]$ , so $f$ is defined on $[- 1, 1]$ . Moreover $1 - b u - (u - b) = (1 + b) (1 - u) \geq 0$ and $1 - b u + (u - b) = (1 - b) (1 + u) \geq 0$ , hence $- 1 \leq f (u) \leq 1$ . The map $g (y) : = (y + b) / (1 + b y)$ is likewise defined on $[- 1, 1]$ , and the comparisons $1 + b y - (y + b) = (1 - b) (1 - y) \geq 0$ and $1 + b y + (y + b) = (1 + b) (1 + y) \geq 0$ show $- 1 \leq g (y) \leq 1$ , so $g$ maps $[- 1, 1]$ into itself; direct expansion of the rational expressions gives $f (g (y)) = [(y + b) - b (1 + b y)] / [(1 + b y) - b (y + b)] = [y (1 - b^{2})] / (1 - b^{2}) = y$ and symmetrically $g (f (u)) = u$ for all $u, y \in [- 1, 1]$ , so $f$ is a bijection of $[- 1, 1]$ onto itself with inverse $g$ . For $v > u$ in $[- 1, 1]$ one has $f (v) - f (u) = [(v - b) (1 - b u) - (u - b) (1 - b v)] / [(1 - b v) (1 - b u)] = (v - u) (1 - b^{2}) / [(1 - b v) (1 - b u)] > 0$ , so $f$ is strictly increasing; in particular $f$ is the stated strictly increasing bijection of $[- 1, 1]$ onto itself, with $f (- 1) = - 1$ and $f (1) = 1$ , and $u = 0$ gives $u^{'} = f (0) = - b = - ∣ β ∣$ .

4.1step 1.1step 2.1step 3.1step 3.2step 3.3step 3.4L2L3L5∎

Clause (vi), $β = 0$ , and scope. If $β = 0$ then $B (0) = id$ by [L3], so $x^{'} = x + b$ is a pure translation; by [L2] the frame data agree, $ϖ^{'} = ϖ$ and $s^{'} = s$ , whence $ω^{'} = ω$ and the x- and x'-inertial axes carry the same wave data, while the affine phase constant changes as follows: since $β = 0$ gives $x^{' a} = x^{a} + b^{a}$ and [L5] gives $k^{'} = k$ , comparing the two chart forms $θ (p) = k_{a} x^{a} (p) + θ (o)$ and $θ (p) = k_{a}^{'} x^{' a} (p) + θ (o^{'})$ of the affine phase yields $θ (o^{'}) = θ (o) - k_{a}^{'} b^{a}$ . All clauses (i)-(v) were derived from the adopted postulates [A1], [A2], [A3] and the cited mathematical lemmas, are conditional on the idealizations recorded in [A1]-[A3] and the scope clause, and make no measurement, statistical or empirical claim; no choice principle was used.

RemarkRemark: AI-adaptedProof: AI-adaptedOpen item page →

Units, coordinate conventions and c restoration for the wave and Doppler formulas

Physical scope

Units and c-restoration conventions for the ideal plane-wave model of flat classical special-relativistic spacetime and its Doppler and aberration formulas. A conventions statement; it asserts no empirical content and excludes quantum energy identifications, amplitudes, intensities and measurement claims.

Remark

Remark on the conventions of SI units and coordinate conventions of the special-relativity framework and Null wave covectors, frame frequency data and the observer frequency of an ideal plane wave, for use with Doppler shift and aberration for an ideal plane wave between inertial descriptions. The frame data and wave data of a future null wave covector are related as in Frame data of a future null wave covector: the unique pair $(ϖ, s)$ with $∣ s ∣ = 1$ , and the symbols below have the meanings fixed there and in Affine phase functions and wave covectors on affine Minkowski space.

(a) Units in the adopted coordinates $x^{0} = c t$ . The phase $θ$ is dimensionless; the coordinates $x^{a}$ , the wavelength $λ$ and all distances are in metres; the components $k_{a}$ of a wave covector, the wave vector $κ$ and $ϖ = - k (e_{0})$ are in $m^{- 1}$ ; the angular frequencies $ω$ and $ω_{n}$ and the linear frequencies $ν$ are in $s^{- 1}$ ( $ν$ also in hertz); $c$ is in $m s^{- 1}$ ; and $s$ , $β$ , $β_{w}$ and $γ$ are dimensionless. These assignments are consistent with the identities $ω = c ϖ$ , $κ = (ω / c) s$ , $λ = 2 π c / ω = c / ν$ and phase $= θ$ dimensionless.

(b) Two coordinate forms. In the adopted coordinates $θ = - ω t + κ \cdot x_{v e c} + c o n s t$ and $k_{a} = (- ω / c, (ω / c) s_{1}, (ω / c) s_{2}, (ω / c) s_{3})$ ; in a chart whose time coordinate is $t$ in seconds directly, so that the metric component $g_{t t} = - c^{2}$ carries $m^{2} s^{- 2}$ and the time-space components carry $m s^{- 1}$ , the same phase is $θ = - ω t + κ \cdot x_{v e c} + c o n s t$ with the same $ω$ and $κ$ , and the component tuple $(- ω, (ω / c) s)$ carries mixed units $(s^{- 1}, m^{- 1})$ because it is read in the coordinate basis $(\partial_{t}, \partial_{x^{i}})$ rather than in the dimensionless frame basis $(e_{0}, e_{1}, e_{2}, e_{3})$ . Formulas derived in one convention are not reused unchanged in the other; this is the general warning of SI units and coordinate conventions of the special-relativity framework specialized to the wave covector.

(c) Natural units and restoration. In natural units $c = 1$ with $x^{0} = t$ one has $k_{a} = (- ω, ω s)$ , $λ = 2 π / ω$ , and the Doppler and aberration factors $γ (1 - β \cdot s)$ and $\sqrt{(1 \mp ∣ β ∣) / (1 \pm ∣ β ∣)}$ are unchanged; restoring dimensions means replacing $k_{0}$ by $- ω / c$ , $k_{i}$ by $(ω / c) s_{i}$ , writing every velocity as $v = c β$ with the dimensionless $β$ , and replacing $λ$ by $2 π c / ω = c / ν$ . The dimensionless factors $γ (1 - β \cdot s)$ and the longitudinal square roots need no $c$ restoration because they contain only $β$ , $s$ and $γ$ ; the $c$ restoration affects the map between $ω$ , $ν$ , $λ$ and the components of $k$ , not the shift factors themselves.

(d) Scope. This remark introduces no quantum identification of energy with $ℏ ω$ , no amplitude or intensity content and no measurement claim; it is a units and convention statement carrying the scope of the items it cites. No choice principle is used.

5 · Examples, experiments and counterexamples

None yet.

Light and Doppler

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

The metric pairing is a linear bijection to the dual, and the raised covector in an orthonormal frame

Statement

Facts & Assumptions

Proof

Affine phase functions and wave covectors on affine Minkowski space

Definition

A future timelike vector pairs negatively with every nonzero future causal vector

Statement

Facts & Assumptions

Proof

Frame data of a future null wave covector: the unique pair (ϖ,s)(ϖ,s) with ∣s∣=1∣s∣=1

Statement

Facts & Assumptions

Proof

Boost transformation of a future null wave covector and of its frame data

Statement

Facts & Assumptions

Proof

The phase rate along a worldline is the wave covector evaluated on the four-velocity

Statement

Facts & Assumptions

Proof

Null wave covectors, frame frequency data and the observer frequency of an ideal plane wave

Definition

Adopted ideal plane-wave and frequency-reading model

Postulate

Doppler shift and aberration for an ideal plane wave between inertial descriptions

Statement

Facts & Assumptions

Proof

Units, coordinate conventions and c restoration for the wave and Doppler formulas

Remark

5 · Examples, experiments and counterexamples

Sources

Frame data of a future null wave covector: the unique pair $(ϖ, s)$ with $∣ s ∣ = 1$