Physics theoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Radar synchronization of an inertial observer reproduces its inertial chart

Physical scope

The statement is conditional on the adopted ideal-clock and ideal-light postulates and on the SI coordinate conventions of the model; it concerns one inertial observer's straight worldline and those events off its axis whose spatial coordinates are nonzero, and it concludes only that the two-way radar protocol of the observer reproduces the inertial chart's time and rest-frame distance. It asserts no one-way light-speed measurement without a synchronization convention, no empirical calibration, no deviation from the ideal model, and nothing about accelerated, rotating, dispersive or finite-resolution situations. The idealizations of the postulates are carried into the conclusion.

Statement

Adopt Adopted ideal-clock and ideal-vacuum-light interpretation (ideal clocks read proper time; ideal vacuum light rays are exactly the future null straight lines) and the SI conventions of SI units and coordinate conventions of the special-relativity framework. Let $(o; e_{0}, e_{1}, e_{2}, e_{3})$ be an inertial frame with chart $x$ , put $n : = e_{0}$ (future unit, $η (n, n) = - 1$ ) and let $W : = x^{- 1} ({(λ, 0, 0, 0) : λ \in R})$ be the coordinate axis, a straight future timelike worldline whose proper time between the events with coordinates $(λ_{-}, 0, 0, 0)$ and $(λ_{+}, 0, 0, 0)$ is $(λ_{+} - λ_{-}) / c$ up to an additive constant (Proper time along a future timelike worldline, Inertial frames and inertial charts of the affine Minkowski model). Let $q$ be an event whose spatial coordinates $r : = (x^{1} (q), x^{2} (q), x^{3} (q))$ are nonzero, and put $λ_{\pm} : = x^{0} (q) \pm ∣ r ∣$ with $∣ r ∣$ the Euclidean norm of The Euclidean spatial structure and cross product of an inertial frame. Then:

(i) the events $e_{-} : = x^{- 1} (λ_{-}, 0, 0, 0)$ and $e_{+} : = x^{- 1} (λ_{+}, 0, 0, 0)$ lie on $W$ , and $q - e_{-}$ , $e_{+} - q$ are future null; hence the radar protocol of The operational radar protocol of an ideal observer applies with emission $e_{-}$ , reflection $q$ and reception $e_{+}$ ;

(ii) the radar assignments are $τ_{r a d} (q) = x^{0} (q) / c$ and $ρ_{r a d} (q) = ∣ r ∣$ up to the additive constant of the observer's proper time: the radar time is the chart time of $q$ and the radar distance is the chart's rest-frame distance;

(iii) consequently, on the region of events with nonzero spatial part, radar simultaneity of this observer coincides with chart simultaneity (equal radar times are equal $x^{0}$ ), and the radar distance equals the rest distance in the simultaneity slice $H (m, n)$ of the midpoint event $m : = x^{- 1} (x^{0} (q), 0, 0, 0)$ (Simultaneity slices and rest distance relative to a future unit timelike vector);

(iv) scope and qualification: this is a conditional statement of the adopted ideal model, showing that the operational round-trip protocol reproduces the inertial chart's time and rest distance, so the operational content of inertial simultaneity is this two-way radar convention; it asserts no one-way light-speed measurement without a synchronization convention, no empirical calibration, no result for accelerated, rotating or dispersive situations, and no deviation from the model. The idealizations of the postulates are carried into the conclusion.

Facts & Assumptions

Given: The adopted ideal-clock and ideal-light postulates and SI conventions (Adopted ideal-clock and ideal-vacuum-light interpretation, SI units and coordinate conventions of the special-relativity framework), an inertial frame $(o; e_{0}, e_{1}, e_{2}, e_{3})$ with chart $x$ , $n = e_{0}$ , the axis $W$ , an event $q$ with $λ_{\pm} : = x^{0} (q) \pm ∣ r ∣$ and $∣ r ∣ > 0$ , and the events $e_{\pm} : = x^{- 1} (λ_{\pm}, 0, 0, 0)$ (Inertial frames and inertial charts of the affine Minkowski model, Oriented time-oriented affine Minkowski space (the spacetime primitives)).

[F1]

Ideal light in vacuum: the ideal light rays are exactly the future null straight lines ${p + μ v : μ \in R}$ with $v$ future null; ideal clocks read the proper time $τ (b) - τ (a) = c^{- 1} \int_{a}^{b} \sqrt{- η (x^{'}, x^{'})} d s$ (Adopted ideal-clock and ideal-vacuum-light interpretation, Proper time along a future timelike worldline).

[F2]

The radar protocol assigns $τ_{r a d} (q) = \frac{1}{2} (τ (s_{-}) + τ (s_{+}))$ and $ρ_{r a d} (q) = \frac{c}{2} (τ (s_{+}) - τ (s_{-}))$ to an event $q$ reached by a future null segment from $e_{-} = x (s_{-})$ and connected to $e_{+} = x (s_{+})$ by a future null segment (The operational radar protocol of an ideal observer).

[F3]

Radar midpoint lemma: for a future unit $n$ , events $e_{\pm} = o + λ_{\pm} n$ with $λ_{-} < λ_{+}$ and an event $q$ , the conditions $q - e_{-}$ , $e_{+} - q$ future null hold if and only if $q = o + \frac{λ_{-} + λ_{+}}{2} n + u$ with $u \in n^{⊥}$ , $∣ u ∣ = (λ_{+} - λ_{-}) / 2$ ; in that case the midpoint is $m = \frac{e_{-} + e_{+}}{2}$ and $d_{n} (m, q) = ∣ u ∣$ in the slice $H (m, n)$ (The radar round trip of an inertial observer halves at the midpoint of the reception interval, Simultaneity slices and rest distance relative to a future unit timelike vector).

[F4]

In the chart of an inertial frame, $x^{0} = c t$ , the metric is $diag (- 1, 1, 1, 1)$ , $η (e_{a}, e_{b}) = diag (- 1, 1, 1, 1)_{a b}$ , and the spatial part of a displacement is measured by the Euclidean norm of The Euclidean spatial structure and cross product of an inertial frame; the axis $W$ is the straight worldline $λ \mapsto o + λ e_{0}$ , whose tangent $e_{0}$ is future unit (Inertial frames and inertial charts of the affine Minkowski model, Curves, regular causal curves and future timelike worldlines in affine Minkowski space, Timelike, null, spacelike and causal vectors of a Lorentz vector space).

Proof

technique · direct

1.1F1F4

With $o : = x^{- 1} (0, 0, 0, 0)$ the axis is $W = {o + λ e_{0} : λ \in R}$ and $e_{\pm} = x^{- 1} (λ_{\pm}, 0, 0, 0) = o + λ_{\pm} e_{0}$ ; the tangent of $W$ is the constant vector $e_{0} = n$ with $η (n, n) = - 1$ , so $W$ is a straight future timelike worldline and its proper-time function satisfies $τ^{'} (λ) = c^{- 1} \sqrt{1} = 1 / c$ , hence $τ (λ) = λ / c + c o n s t$ by [F1] and [F4].

2.1F1F2F3F4step 1.1

The hypotheses of the radar midpoint lemma [F3] are satisfied with $λ_{\pm} = x^{0} (q) \pm ∣ r ∣$ : since $∣ r ∣ = 0$ is excluded, $λ_{-} < λ_{+}$ ; the event $q$ has displacement $q - o = x^{0} (q) n + r_{1} e_{1} + r_{2} e_{2} + r_{3} e_{3}$ by [F4], so $q = o + \frac{λ_{-} + λ_{+}}{2} n + u$ with $u : = r_{1} e_{1} + r_{2} e_{2} + r_{3} e_{3} \in n^{⊥}$ and $∣ u ∣ = ∣ r ∣ = (λ_{+} - λ_{-}) / 2$ , because $e_{1}, e_{2}, e_{3}$ span $n^{⊥}$ and the norm of $u$ is the Euclidean norm of the spatial part by [F4]. By [F3] the displacements $q - e_{-}$ and $e_{+} - q$ are future null; hence the radar protocol applies with emission $e_{-}$ , reflection $q$ and reception $e_{+}$ by [F2].

3.1F2step 1.1step 2.1

The radar assignments of clause (ii): by [F2] and step 2.1, $τ_{r a d} (q) = \frac{1}{2} (τ (λ_{-}) + τ (λ_{+}))$ and $ρ_{r a d} (q) = \frac{c}{2} (τ (λ_{+}) - τ (λ_{-}))$ , and substituting the proper-time function of step 1.1 gives $τ_{r a d} (q) = \frac{λ_{-} + λ_{+}}{2 c} + c o n s t = \frac{x^{0} (q)}{c} + c o n s t$ and $ρ_{r a d} (q) = \frac{c}{2} \cdot \frac{λ_{+} - λ_{-}}{c} = \frac{λ_{+} - λ_{-}}{2} = ∣ r ∣$ , where the additive constant is the same for all events measured by this observer. Hence the radar time is the chart time and the radar distance is the chart's rest-frame distance, up to the fixed additive constant of the following.

4.1F3step 2.1step 3.1

Clause (iii): by [F3] and step 2.1 the midpoint of the round trip is $m = \frac{e_{-} + e_{+}}{2} = x^{- 1} (x^{0} (q), 0, 0, 0)$ , the displacement $q - m = u$ lies in $n^{⊥}$ , and the rest distance in the slice $H (m, n)$ is $d_{n} (m, q) = ∣ u ∣ = ∣ r ∣$ , which equals $ρ_{r a d} (q)$ by step 3.1; and since $τ_{r a d}$ differs from $x^{0} / c$ by a constant depending only on the observer, two events measured by this observer have equal radar times if and only if they have equal chart time $x^{0}$ , so radar simultaneity coincides with chart simultaneity on the stated region.

5.1step 1.1step 2.1step 3.1step 4.1∎

Conclusion and scope: steps 1.1 and 2.1 prove (i) — the events $e_{\pm}$ lie on the observer's worldline and the two displacements are future null, so the operational protocol applies; steps 3.1 and 4.1 prove (ii) and (iii); clause (iv) is the honest qualification of the result: the deduction is conditional on the adopted ideal-clock and ideal-light postulates and the SI conventions, it identifies the operational content of inertial simultaneity as the two-way radar convention, and it asserts no one-way light-speed measurement without a synchronization convention, no empirical calibration and no result for accelerated, rotating or dispersive situations.

Remarks

Conditional status. The theorem is a conditional deduction inside the ideal model: the hypotheses are the adopted postulates, not experimental facts, and the conclusion is a statement about the model's own operational assignment. No measurement, calibration or statistical comparison is asserted, and the idealizations (exact proper-time readings, exact future null straight rays, instantaneous reflection) are part of the scope carried into every consumer.
What the symmetric split achieves. The radar time $\frac{1}{2} (λ_{-} + λ_{+}) / c$ is the half-sum of the emission and reception chart times, and the radar distance is half the round-trip light time times $c$ ; the theorem shows that these two-way quantities reproduce the chart's time coordinate and Euclidean rest distance. The one-way split into an outgoing and a returning light time is the symmetric convention fixed in The operational radar protocol of an ideal observer and is not measured independently.

Radar synchronization of an inertial observer reproduces its inertial chart

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources