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.

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.

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

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

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

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

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