LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

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.

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

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources