Physlib.Relativity.Tensors.RealTensor.Vector.Causality.Basic

The inductive type `CausalCharacter` represents the classification of a Lorentz vector $p$ in Minkowski space according to its causal nature. It categorizes vectors into three possible cases based on the sign of the Minkowski inner product $p^2$ (or $p \cdot p$): **timelike** ($p^2 > 0$), **spacelike** ($p^2 < 0$), and **null** or lightlike ($p^2 = 0$).

The equality of causal characters—which classify Lorentz vectors as **timelike** ($p^2 > 0$), **spacelike** ($p^2 < 0$), or **null** ($p^2 = 0$)—is decidable. That is, for any two causal characters $c_1$ and $c_2$, it can be determined whether $c_1 = c_2$ or $c_1 \neq c_2$.

For a Lorentz vector $p \in \text{Vector}_d$ in a Minkowski space with $d$ spatial dimensions, its causal character is defined by the sign of its Minkowski inner product $\langle p, p \rangle_m$ (using the $+ - - -$ metric signature). The vector $p$ is classified as: - **lightlike** (or null) if $\langle p, p \rangle_m = 0$, - **timelike** if $\langle p, p \rangle_m > 0$, - **spacelike** if $\langle p, p \rangle_m < 0$.

For any Lorentz vector $p \in \text{Vector}_d$ in a Minkowski space with $d$ spatial dimensions and any Lorentz transformation $\Lambda \in \text{LorentzGroup}_d$, the causal character of the vector $\Lambda \cdot p$ is equal to the causal character of $p$. The causal character classifies $p$ based on its Minkowski inner product $\langle p, p \rangle_m$ as: - **lightlike** (or null) if $\langle p, p \rangle_m = 0$, - **timelike** if $\langle p, p \rangle_m > 0$, - **spacelike** if $\langle p, p \rangle_m < 0$.

Let $p$ be a Lorentz vector in a Minkowski space with $d$ spatial dimensions. The causal character of $p$ is spacelike if and only if its Minkowski inner product $\langle p, p \rangle_m$ is strictly less than zero.

For any Lorentz vector $p \in \text{Vector}_d$ in a Minkowski space with $d$ spatial dimensions, the causal character of the negated vector $-p$ is the same as the causal character of $p$. That is, $\text{causalCharacter}(-p) = \text{causalCharacter}(p)$.

For a Lorentz vector $p$ in a Minkowski space with $d$ spatial dimensions, the interior future light cone of $p$ is the set of vectors $q$ such that the displacement vector $q - p$ is timelike (meaning its Minkowski inner product satisfies $\langle q - p, q - p \rangle_m > 0$) and the time component of this displacement, $(q - p)^0$, is positive.

For a Lorentz vector $p$ in a Minkowski space with $d$ spatial dimensions, the interior past light cone is the set of vectors $q$ such that the displacement vector $q - p$ is timelike (i.e., its Minkowski inner product satisfies $\langle q - p, q - p \rangle_m > 0$) and the time component of the displacement, $(q - p)_0$, is negative.

For a given Lorentz vector $p \in \text{Vector}_d$ in a Minkowski space with $d$ spatial dimensions, the light cone boundary (or null surface) of $p$ is the set of all vectors $q \in \text{Vector}_d$ such that the displacement vector $q - p$ is lightlike (null). Formally, this is the set $\{q \in \text{Vector}_d \mid \langle q - p, q - p \rangle_m = 0\}$, where $\langle \cdot, \cdot \rangle_m$ denotes the Minkowski inner product.

For a spacetime point $p$ in a Minkowski space with $d$ spatial dimensions, the future light cone boundary is the set of all points $q$ such that the displacement vector $q - p$ is lightlike (null), meaning its Minkowski inner product $\langle q - p, q - p \rangle_m = 0$, and its temporal component (indexed by `Sum.inl 0`) is non-negative, i.e., $(q - p)^0 \geq 0$.

For a spacetime point $p$ in the $d$-dimensional Lorentz vector space $\text{Vector}_d$, the past light cone boundary (also known as the past null surface) is the set of all vectors $q \in \text{Vector}_d$ such that the displacement vector $q - p$ is lightlike and its temporal component is non-positive. Formally, this is the set $\{q \in \text{Vector}_d \mid \text{causalCharacter}(q - p) = \text{lightlike} \text{ and } (q - p)_0 \le 0\}$, where $(\cdot)_0$ denotes the time component of the vector.

For any Lorentz vector $p \in \text{Vector}_d$ in a Minkowski space with $d$ spatial dimensions, $p$ belongs to its own light cone boundary.

For two events $p, q$ represented as Lorentz vectors in a Minkowski space with $d$ spatial dimensions, $q$ **causally follows** $p$ if $q$ belongs to the causal future of $p$. This is defined as $q$ being an element of either the interior future light cone of $p$ (where the displacement $q-p$ is timelike and $(q-p)^0 > 0$) or the future light cone boundary of $p$ (where $q-p$ is lightlike and $(q-p)^0 \geq 0$).

For two events $p$ and $q$ in a $d$-dimensional Minkowski space $\text{Vector}_d$, the proposition $q$ causally precedes $p$ is true if $q$ lies within the interior of the past light cone of $p$ or on its boundary. This is equivalent to stating that the displacement vector $q - p$ is non-spacelike (i.e., its Minkowski inner product satisfies $\langle q - p, q - p \rangle_m \ge 0$) and the temporal component of the displacement $(q - p)_0$ is non-positive.

For two events $p, q$ in a Minkowski space with $d$ spatial dimensions, $p$ and $q$ are **causally related** if either $q$ causally follows $p$ or $p$ causally follows $q$. This is equivalent to saying that the displacement vector $q - p$ is non-spacelike (timelike or lightlike), satisfying the Minkowski inner product condition $\langle q - p, q - p \rangle_m \ge 0$.

Two events $p, q \in \text{Vector}_d$ in Minkowski space are causally unrelated (or spacelike separated) if the causal character of their difference $p - q$ is spacelike. This corresponds to the condition that the Minkowski inner product of the displacement vector is negative, $\langle p - q, p - q \rangle_m < 0$, given the metric signature $(+,-,-,\dots)$.

For two events $p, q$ in Minkowski spacetime with $d$ spatial dimensions, the causal diamond between $p$ and $q$ is the set of all events $r \in \text{Vector}_d$ such that $r$ causally follows $p$ and $q$ causally follows $r$. Mathematically, this is the set $\{r \mid p \preceq r \text{ and } r \preceq q\}$, which represents the intersection of the causal future of $p$ and the causal past of $q$. Here, the relation $x \preceq y$ (causally follows) indicates that the displacement vector $y - x$ is either timelike or lightlike and is future-directed (having a non-negative temporal component $(y-x)^0 \geq 0$).

In Minkowski spacetime with $d$ spatial dimensions and metric signature $(+,-,-,\dots)$, a Lorentz vector $v$ is future-directed if its temporal component $v^0$ is strictly positive, i.e., $v^0 > 0$.

In Minkowski spacetime with $d$ spatial dimensions and metric signature $(+,-,-,\dots)$, a Lorentz vector $v$ is past-directed if its temporal component $v^0$ is strictly negative, i.e., $v^0 < 0$.