ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck pending

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.

Worked null corner: two non-parallel null legs compose to a timelike displacement and push up to strict chronology

Example

Assume Countable Choice and Dependent Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ ), The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain) for the causal reachability and supplied causal-calculus conclusions used here.

In the flat model $(A, η, N)$ with global inertial chart $x = (t, y_{1}, y_{2}, y_{3})$ , put $p : = x^{- 1} (0, 0, 0, 0)$ , $q : = x^{- 1} (1, 1, 0, 0)$ and $r : = x^{- 1} (2, 0, 0, 0)$ . The straight paths $p \to q$ and $q \to r$ are null, so $p \leq q \leq r$ , while the total displacement $r - p = (2, 0, 0, 0)$ is future timelike. This example verifies the two conclusions of the push-up rule The push-up rule: p << q and q <= r imply p << r, together with the timelike-piece criterion in this explicit configuration: $p ≪ r$ , with an explicit future timelike curve from $p$ to $r$ ; and it contrasts the non-parallel case with the parallel case, in which the composition of two null legs stays null.

Facts & Assumptions

Given: The flat model with inertial chart $x$ and the events $p = x^{- 1} (0, 0, 0, 0)$ , $q = x^{- 1} (1, 1, 0, 0)$ , $r = x^{- 1} (2, 0, 0, 0)$ , $r^{'} = x^{- 1} (2, 2, 0, 0)$ .

[L1]

Inertial cone criterion: a nonzero displacement $v$ is future timelike, future null or future causal exactly when $v^{0} > ∣ v_{v e c} ∣$ , $v^{0} = ∣ v_{v e c} ∣$ , or $v^{0} \geq ∣ v_{v e c} ∣$ (and then $v^{0} > 0$ because $v \neq 0$ ); the straight path $s \mapsto x^{- 1} (a + s v)$ is a geodesic with constant velocity $v$ and hence, when $v$ is future causal, a future causal curve (The causal cones of the flat model in inertial coordinates, and closure of the future cone under sums, The flat model: Minkowski space R^4, its standard Lorentz form, inertial charts and cone sets, Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones, Causal curves, chronological and causal reachability, and inextendibility).

[L2]

A smooth curve with future timelike velocity everywhere is a future timelike curve; velocities are read in the inertial chart by differentiating the chart representative (Chart independence, concatenation, reparametrization and transitivity for causal curves clause (c), The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ , $C^{r}$ and smooth maps between smooth manifolds).

[L3]

Push-up: if $u ≪ u^{'}$ and $u^{'} \leq u^{''}$ then $u ≪ u^{''}$ ; moreover if a future causal curve from $u$ to $u^{''}$ has a timelike piece then $u ≪ u^{''}$ (The push-up rule: p << q and q <= r imply p << r, together with the timelike-piece criterion).

Proof

technique · direct

1.1L1given

(The two legs are future null.) The displacements are $q - p = (1, 1, 0, 0)$ and $r - q = (1, - 1, 0, 0)$ ; both satisfy $v^{0} = ∣ v_{v e c} ∣ = 1 > 0$ , hence both are future null by [L1], and the corresponding straight paths are future causal curves. Therefore $p \leq q$ and $q \leq r$ , and consequently $p \leq r$ .

2.1step 1.1L1

(The total displacement is future timelike.) The displacement $r - p = (2, 0, 0, 0)$ satisfies $v^{0} = 2 > 0 = ∣ v_{v e c} ∣$ , hence is future timelike by [L1]. In particular $r \neq p$ .

2.2step 1.1L1given

(Contrast: the parallel case stays null.) For $r^{'} = x^{- 1} (2, 2, 0, 0)$ the second displacement $r^{'} - q = (1, 1, 0, 0)$ is a positive multiple of the first, the broken path is the straight null path from $p$ to $r^{'}$ (the two legs are collinear), and $r^{'} - p = (2, 2, 0, 0)$ satisfies $v^{0} = ∣ v_{v e c} ∣ = 2$ , so it is future null: in the parallel case the composition of two null legs remains null, and no strict chronology follows. This shows why the non-parallel corner is exactly what produces the timelike total displacement.

3.1step 2.1L1L2L3

(Strict chronology by the straight path and by an explicit curve.) The displacement $r - p = (2, 0, 0, 0)$ satisfies $v^{0} = 2 > 0 = ∣ v_{v e c} ∣$ , so it is future timelike by [L1]; hence the straight path $σ (s) : = x^{- 1} (x (p) + s (r - p))$ , $s \in [0, 1]$ , has the constant future timelike velocity $r - p$ and is a smooth future timelike curve from $p$ to $r$ , so $p ≪ r$ [L1, L2]. As an independent certificate, $γ (s) : = x^{- 1} (s, \frac{1}{4} \sin (π s), 0, 0)$ on $[0, 2]$ is smooth with chart velocity $(1, \frac{π}{4} \cos (π s), 0, 0)$ of spatial norm at most $π / 4 < 1$ , hence future timelike everywhere by [L1]; it runs from $γ (0) = p$ to $γ (2) = r$ . Since $γ$ is a future causal curve carrying a timelike piece, clause (c) of the push-up rule The push-up rule: p << q and q <= r imply p << r, together with the timelike-piece criterion equally yields $p ≪ r$ , in agreement with the direct computation.

4.1step 3.1step 2.2step 2.1∎

(Summary.) For the non-parallel null legs the two legs give $p \leq q \leq r$ while the total displacement is future timelike, and $p ≪ r$ is certified both by the straight path and by the explicit timelike curve $γ$ ; for parallel null legs the total displacement stays null. This exhibits exactly the strict output that the push-up rule records for a causal connection with a timelike piece.

Remarks

What the example tests. It exercises the strict output of the push-up rule: causality alone gives $p \leq r$ , and only the non-collinear corner upgrades the relation to $p ≪ r$ .
No empirical content. The computation is a mathematical verification in the flat model and reports no observation.

Depends on

Dependency tree · 2 levels

Sources

E. Minguzzi, Lorentzian causality theory, Living Reviews in Relativity 22 (2019) 3: the push-up rule and the strict timelike conclusion from a null corner, section 1.11 printed pp. 15-16 and section 2.6