ExampleConstruction: AI-adaptedVerification: AI-generatedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

A prearranged sweep with superluminal coordinate speed: successive events are spacelike separated and can be made simultaneous

Example

Worked computation in the chart $x$ of an inertial frame with $x^{0}$ in metres and $c > 0$ (Inertial frames and inertial charts of the affine Minkowski model). Fix $w > c$ and consider the family $E_{ξ} : = x^{- 1} (\frac{c}{w} ξ, ξ, 0, 0), ξ \in R,$ a prearranged array of devices at $x^{1} = ξ$ triggered at coordinate time $t = ξ / w$ , so the pattern is a sweep of coordinate speed $w > c$ along the row.

(a) For $ξ < η$ the displacement is $E_{η} - E_{ξ} = (\frac{c}{w} (η - ξ), η - ξ, 0, 0),$ whose interval is $(η - ξ)^{2} (1 - c^{2} / w^{2}) > 0$ , so successive events are spacelike separated; in particular no event $E_{η}$ lies in $J^{+} (E_{ξ})$ or $J^{-} (E_{ξ})$ for $η \neq ξ$ , by the coordinate criterion (The closed future cone in inertial coordinates: description, finite sums, and the coordinate criterion for causal reachability).

(b) Let $b : = c / w \in (0, 1)$ . The passive boost with parameter $b e_{1}$ (The passive Lorentz boost with parameter beta) maps the displacement to time component $γ_{b} (\frac{c}{w} (η - ξ) - b (η - ξ)) = γ_{b} (η - ξ) (\frac{c}{w} - \frac{c}{w}) = 0$ , so in the boosted chart $x_{b}$ the whole family consists of events simultaneous at one coordinate time; taking $b > c / w$ produces the opposite sign $γ_{b} (η - ξ) (\frac{c}{w} - b)$ , so the apparent temporal order of the sweep runs forward, frozen or backward in different inertial frames even though no event of the family is causally related to another (Spacelike-separated events: the spacelike coordinate inequality in every inertial chart, and an explicit family of inertial frames realizing every time-order sign).

(c) No signal statement is made or needed: the computation is a property of the spacetime locations of independently triggered events, and it exhibits the class of spacelike-separated patterns that a kinematic superluminal speed bound cannot exclude. It is a statement about the locations of the events, it asserts nothing about any of them being the reception of a signal, and it does not model the fixed-speed relay kinematics of the hypothetical superluminal model treated on the companion page.

Facts & Assumptions

Given: An inertial frame with chart $x$ and origin event $o = x^{- 1} (0, 0, 0, 0)$ , a constant $c > 0$ , a real $w > c$ , the family $E_{ξ} = x^{- 1} ((c / w) ξ, ξ, 0, 0)$ of events, and for $∣ b ∣ < 1$ the boost $B (b e_{1})$ with $γ_{b} = (1 - b^{2})^{- 1 / 2}$ .

[L1]

For the spacelike pair $(E_{0}, E_{1})$ with displacement $D = (c / w, 1, 0, 0)$ and spatial unit direction $e_{1}$ , and for every $∣ b ∣ < 1$ , the chart $x_{b}$ of the inertial frame with the same origin $o$ and basis $e_{a}^{'} : = B (b e_{1})^{- 1} e_{a}$ satisfies $x_{b} = B (b e_{1}) \circ x$ and $x_{b}^{0} (E_{1}) - x_{b}^{0} (E_{0}) = γ_{b} (D^{0} - b ∣ D_{s} ∣)$ ; in general $∣ D^{0} ∣ < ∣ D_{s} ∣$ in every inertial chart (Spacelike-separated events: the spacelike coordinate inequality in every inertial chart, and an explicit family of inertial frames realizing every time-order sign).

[L2]

The passive boost acts in the $(0, 1)$ -plane by $x^{' 0} = γ (x^{0} - b x^{1})$ , $x^{' 1} = γ (x^{1} - b x^{0})$ and is linear in the coordinate column (The passive Lorentz boost with parameter beta).

[L3]

Diagonal form and classification: $η (D, D) = - (D^{0})^{2} + ∣ D_{s} ∣^{2}$ , and $D$ is spacelike exactly when $η (D, D) > 0$ , timelike exactly when $η (D, D) < 0$ (Timelike, null, spacelike and causal vectors of a Lorentz vector space).

[L4]

Coordinate criterion for reachability: for events $r, s$ with $D = x (s) - x (r)$ , $s \in J^{+} (r)$ iff $D^{0} \geq ∣ D_{s} ∣$ , and $s \in J^{-} (r)$ iff $- D^{0} \geq ∣ D_{s} ∣$ (The closed future cone in inertial coordinates: description, finite sums, and the coordinate criterion for causal reachability, Causal reachability, causal futures and pasts, causal diamonds, and reachability by future causal paths in affine Minkowski space).

[L5]

Chart linearity: $x (s) - x (r) = E^{- 1} (s - r)$ for events $r, s$ (Inertial frames and inertial charts of the affine Minkowski model).

Verification

technique · direct

1.1givenL3L4L5algebra

For $ξ < η$ the displacement of the family is $E_{η} - E_{ξ} = ((c / w) (η - ξ), η - ξ, 0, 0)$ by [L5], so $η (E_{η} - E_{ξ}, E_{η} - E_{ξ}) = - (c / w)^{2} (η - ξ)^{2} + (η - ξ)^{2} = (η - ξ)^{2} (1 - c^{2} / w^{2}) > 0$ because $w > c$ and $η - ξ > 0$ ; hence the displacement is spacelike by [L3]. For $η > ξ$ the first criterion of [L4] would require $(c / w) (η - ξ) \geq η - ξ$ , which fails since $c / w < 1$ , and the second would require $- (c / w) (η - ξ) \geq η - ξ$ , which also fails; the case $ξ > η$ is the same computation with the roles exchanged, so no event of the family lies in the causal future or past of another; this is (a).

2.1step 1.1L1L2L5algebra

Set $b : = c / w \in (0, 1)$ . The vector $E_{1} - E_{0}$ is spacelike by step 1.1, so [L1] applies with the origin event $o$ and gives the chart $x_{b} = B (b e_{1}) \circ x$ of an inertial frame; by linearity [L2] and [L5], $x_{b} (E_{η}) - x_{b} (E_{ξ}) = B (b e_{1}) (E_{η} - E_{ξ})$ , whose time component is $γ_{b} ((c / w) (η - ξ) - b (η - ξ)) = γ_{b} (η - ξ) (c / w - c / w) = 0$ for all $ξ, η$ ; hence all events $E_{ξ}$ share the coordinate time $x_{b}^{0}$ . For a parameter $b^{'} > c / w$ with $b^{'} < 1$ , which exists because $c / w < 1$ , the same computation gives $x_{b^{'}}^{0} (E_{η}) - x_{b^{'}}^{0} (E_{ξ}) = γ_{b^{'}} (η - ξ) (c / w - b^{'})$ , of sign opposite to $η - ξ$ ; so the temporal order of the sweep runs forward in $x$ , is frozen in $x_{b}$ and runs backward in $x_{b^{'}}$ ; this is (b).

3.1step 1.1step 2.1given∎

Steps 1.1 and 2.1 compute only the locations and coordinate differences of the family $E_{ξ}$ and the chart changes of those coordinate differences; the family is prearranged and independently triggered, no displacement of the family is causal in either direction, and nothing in the computation identifies an event $E_{ξ}$ with the reception of a signal or with the relay model of the companion page; the sweep is a kinematic pattern whose temporal order is frame-dependent without any causal relation among its events, and no choice principle is used.

A prearranged sweep with superluminal coordinate speed: successive events are spacelike separated and can be made simultaneous

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources