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.
Rindler radar distances worked: reflectors at twice and at half the observer's radius
Worked numerical instance of the conditional Rindler radar protocol for two coaxial uniformly accelerated ideal observers with ideal clocks, ideal light rays and ideal reflectors in flat classical spacetime. No apparatus, measurement, statistical or empirical claim is made, and all idealizations of pthm-sr-rindler-horizons-and-radar are retained.
Example
Worked computation in the Rindler chart of The Rindler chart: causal horizons of a uniformly accelerated observer and the restrictions of radar time and distance. Let , fix and take ; let be the congruence worldline with Rindler time , and take the emission event at , so that in the inertial chart .
(a) Reflector at . The future null line from of constant has , and it meets at the Rindler time ; using and (Addition formulas, identities, parity, and derivatives of the hyperbolic functions, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm) the reflection event is , and the return event is at Rindler time . Thus , the radar time assigned to is plus the base constant of 's proper time, and the radar distance is . The two worldlines and are at rest distance in the slice ; since gives (The elementary numerical bound , Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm), the radar distance is strictly smaller than the rest distance.
(b) Reflector at . The future null line from of constant has , and it meets at the Rindler time ; using and the reflection event is and the return event is again at Rindler time . The radar time is again plus the base constant and the radar distance is again , while the rest distance in the slice is now ; since gives (The elementary numerical bound , Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm), the radar distance is now strictly larger than the rest distance.
(c) The two cases (a)-(b) give the same radar distance at distinct rest distances and ; this demonstrates noninjectivity of the assignment as the reflector radius varies. To prove that radar distance is not determined by the rest distance alone, also take . With the same emission at , the reflection occurs at , at , and the return occurs at , at . This reflector has rest distance , equal to case (b), but radar distance , because and is strictly increasing. These equal inputs and unequal outputs prove the stated failure of dependence on rest distance alone. The original two cases both satisfy and have round-trip proper time ; the third case satisfies the same midpoint identity and has round-trip proper time .
(d) Scope. Conditional model computation with ideal clocks, ideal light rays and ideal reflectors in the flat classical model; no measurement, apparatus, source or statistical claim, and no empirical inference, is made, and the idealizations of The Rindler chart: causal horizons of a uniformly accelerated observer and the restrictions of radar time and distance (v) are retained.
Facts & Assumptions
Given: , , , the inertial chart with , the congruence worldlines (observer ) and (reflector) with Rindler time on , and the emission event at ; the radar protocol of The operational radar protocol of an ideal observer is applied with as observer.
Rindler chart and congruence: and ; the future null lines in the plane of the two worldlines are the constant- lines and the constant- lines; the congruence worldlines have Rindler time up to an additive constant (The Rindler chart: causal horizons of a uniformly accelerated observer and the restrictions of radar time and distance (i),(ii); Inertial frames and inertial charts of the affine Minkowski model, Oriented time-oriented affine Minkowski space (the spacetime primitives)).
Coaxial radar geometry: for a reflector at , the reflection occurs at , the return at with midpoint , the radar distance is , and the radar time is plus a constant (The Rindler chart: causal horizons of a uniformly accelerated observer and the restrictions of radar time and distance (iii), The operational radar protocol of an ideal observer).
Rest distance in a slice: two congruence worldlines and at the same Rindler time are at rest distance (The Rindler chart: causal horizons of a uniformly accelerated observer and the restrictions of radar time and distance (iii), Simultaneity slices and rest distance relative to a future unit timelike vector).
Hyperbolic and logarithmic values: , , , and ; , so and therefore , and is strictly increasing with (The six hyperbolic functions and their natural domains, Addition formulas, identities, parity, and derivatives of the hyperbolic functions, The elementary numerical bound , Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The natural logarithm as the inverse of the exponential function).
Proof technique: direct.
Verification
(Clause (a): the outer reflector.) With and , [L2] gives , so the reflection event is by the values , of [L4], and the return occurs at at using and of [L4]; the midpoint identity and the radar distance follow from [L2]. The rest distance in the slice is by [L3], and because by [L4].
(Clause (b): the inner reflector.) With and , [L2] gives , so the reflection event is by [L4], and the return at is the same event as in step 1.1; the radar distance is again by [L2], while the rest distance in the slice is by [L3]. Since implies by [L4], the radar distance exceeds the rest distance in this case.
(Clause (c): the third reflector and noninjectivity.) With and , [L2] gives ; the hyperbolic values and give the reflection event , and the return at is , using and at by [L4]; the radar distance is , the rest distance in the slice is by [L3] (the same as in step 2.1), and because and is strictly increasing by [L4]. Thus two distinct reflector radii ( and ) share the rest distance but have different radar distances, and the two cases of steps 1.1 and 2.1 share the radar distance at rest distances and .
(Midpoint identities, round-trip times and scope.) In each of the three cases the reported is the midpoint by [L2], and the round-trip proper time of is , equal to in cases (a) and (b) and to in case (c). All quantities are conditional model computations with ideal clocks, light rays and reflectors; no apparatus, measurement or empirical claim is made, and no choice principle was used.
Depends on
The Rindler chart: causal horizons of a uniformly accelerated observer and the restrictions of radar time and distance
The operational radar protocol of an ideal observer
Inertial frames and inertial charts of the affine Minkowski model
Oriented time-oriented affine Minkowski space (the spacetime primitives)
The natural logarithm as the inverse of the exponential function
Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm
The elementary numerical bound
The six hyperbolic functions and their natural domains
Addition formulas, identities, parity, and derivatives of the hyperbolic functions
Simultaneity slices and rest distance relative to a future unit timelike vector
Dependency tree · 2 levels
Sources
- Wikipedia, 'Rindler coordinates': section 'Notions of distance' (the null geodesic equation t - t_0 = log(x/x_0) and the radar distance x_0 log(1 + h/x_0) between Rindler observers at x_0 and x_0 + h, with the rider that radar distance need not be symmetric)
- B. Crowell, Special Relativity, revision 2020-12-10 (author-published undergraduate textbook, 246 PDF pages): Section 3.5.2 and Section 7.1 pp. 61-62 and 147-148 (hyperbolic motion, accelerated coordinates and their horizons, in the convention x^0 = c t); signature (+---) converted to (-+++), c = 1 formulas restored to x^0 = c t