Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge 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.

Rindler radar distances worked: reflectors at twice and at half the observer's radius

Physical scope

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 c>0, fix ρ0>0 and take y0=z0=0; let O be the congruence worldline ρ=ρ0 with Rindler time θ=cτ/ρ0, and take the emission event e− at θe=0, so that e−=x−1(0,ρ0,0,0) in the inertial chart x.

(a) Reflector at ρm=2ρ0. The future null line from e− of constant V has V=−ρ0, and it meets ρ=2ρ0 at the Rindler time θm=log⁡2; using sinh⁡(log⁡2)=3/4 and cosh⁡(log⁡2)=5/4 (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 qm=x−1(3ρ0/2,5ρ0/2,0,0), and the return event is e+=x−1(ρ0sinh⁡(2log⁡2),ρ0cosh⁡(2log⁡2),0,0)=x−1(15ρ0/8,17ρ0/8,0,0) at Rindler time θ(e+)=2log⁡2. Thus (θe+θ(e+))/2=log⁡2=θm, the radar time assigned to qm is (ρ0/c)log⁡2 plus the base constant of O's proper time, and the radar distance is ρ0log⁡2. The two worldlines ρ=ρ0 and ρ=2ρ0 are at rest distance ρ0 in the slice θ=log⁡2; since e>2 gives log⁡2<1 (The elementary numerical bound 2<e<3, 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 ρm=ρ0/2. The future null line from e− of constant U has U=ρ0, and it meets ρ=ρ0/2 at the Rindler time θm=log⁡2; using sinh⁡(log⁡2)=3/4 and cosh⁡(log⁡2)=5/4 the reflection event is qm′=x−1(3ρ0/8,5ρ0/8,0,0) and the return event is again e+=x−1(15ρ0/8,17ρ0/8,0,0) at Rindler time 2log⁡2. The radar time is again (ρ0/c)log⁡2 plus the base constant and the radar distance is again ρ0log⁡2, while the rest distance in the slice θ=log⁡2 is now ρ0/2; since e<3<4 gives log⁡2>1/2 (The elementary numerical bound 2<e<3, 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 ρ0log⁡2 at distinct rest distances ρ0 and ρ0/2; 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 ρm=3ρ0/2. With the same emission at θe=0, the reflection occurs at θm=log⁡(3/2), at qm′′=x−1(5ρ0/8,13ρ0/8,0,0), and the return occurs at 2log⁡(3/2), at e+′′=x−1(65ρ0/72,97ρ0/72,0,0). This reflector has rest distance ρ0/2, equal to case (b), but radar distance ρ0log⁡(3/2)<ρ0log⁡2, because 3/2<2 and log⁡ 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 θm=(θe+θ(e+))/2 and have round-trip proper time 2ρ0log⁡2/c; the third case satisfies the same midpoint identity and has round-trip proper time 2ρ0log⁡(3/2)/c.

(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: c>0, ρ0>0, y0=z0=0, the inertial chart x with x0=ct, the congruence worldlines ρ=ρ0 (observer O) and ρ=ρm (reflector) with Rindler time θ=cτ/ρ0 on O, and the emission event e−=x−1(0,ρ0,0,0) at θe=0; the radar protocol of The operational radar protocol of an ideal observer is applied with O as observer.

[L1]

Rindler chart and congruence: U=ρeθ and V=−ρe−θ; the future null lines in the plane of the two worldlines are the constant-U lines and the constant-V lines; the congruence worldlines have Rindler time θ=cτ/ρ 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)).

[L2]

Coaxial radar geometry: for a reflector at ρm≠ρ0, the reflection occurs at θm=θe+∣log⁡(ρm/ρ0)∣, the return at θ(e+)=θe+2∣log⁡(ρm/ρ0)∣ with midpoint θm, the radar distance is ρ0∣log⁡(ρm/ρ0)∣, and the radar time is (ρ0/c)θm 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).

[L3]

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).

[L4]

Hyperbolic and logarithmic values: sinh⁡u=(eu−e−u)/2, cosh⁡u=(eu+e−u)/2, sinh⁡(x+y)=sinh⁡xcosh⁡y+cosh⁡xsinh⁡y, cosh⁡(x+y)=cosh⁡xcosh⁡y+sinh⁡xsinh⁡y and cosh⁡u+sinh⁡u=eu; 2<e<3<4, so log⁡2<log⁡e=1<log⁡4=2log⁡2 and therefore 1/2<log⁡2<1, and log⁡ is strictly increasing with log⁡(3/2)<log⁡2 (The six hyperbolic functions and their natural domains, Addition formulas, identities, parity, and derivatives of the hyperbolic functions, The elementary numerical bound 2<e<3, 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

1.1L1L2L3L4algebra

(Clause (a): the outer reflector.) With ρm=2ρ0 and θe=0, [L2] gives θm=log⁡2, so the reflection event is qm=(2ρ0sinh⁡log⁡2,2ρ0cosh⁡log⁡2,0,0)=(3ρ0/2,5ρ0/2,0,0) by the values sinh⁡log⁡2=3/4, cosh⁡log⁡2=5/4 of [L4], and the return occurs at θ(e+)=2log⁡2 at e+=(ρ0sinh⁡(2log⁡2),ρ0cosh⁡(2log⁡2),0,0)=(15ρ0/8,17ρ0/8,0,0) using sinh⁡(2log⁡2)=2⋅(3/4)(5/4)=15/8 and cosh⁡(2log⁡2)=(25+9)/16=17/8 of [L4]; the midpoint identity and the radar distance ρ0log⁡2 follow from [L2]. The rest distance in the slice θ=log⁡2 is ∣2ρ0−ρ0∣=ρ0 by [L3], and ρ0log⁡2<ρ0 because log⁡2<1 by [L4].

2.1L2L3L4step 1.1algebra

(Clause (b): the inner reflector.) With ρm=ρ0/2 and θe=0, [L2] gives θm=log⁡(ρ0/ρm)=log⁡2, so the reflection event is qm′=(ρ0/2)(3/4,5/4,0,0)=(3ρ0/8,5ρ0/8,0,0) by [L4], and the return at θ(e+)=2log⁡2 is the same event e+=(15ρ0/8,17ρ0/8,0,0) as in step 1.1; the radar distance is again ρ0log⁡2 by [L2], while the rest distance in the slice θ=log⁡2 is ∣ρ0−ρ0/2∣=ρ0/2 by [L3]. Since 2<e<3<4 implies log⁡2>1/2 by [L4], the radar distance exceeds the rest distance in this case.

3.1L1L2L3L4step 1.1step 2.1algebra

(Clause (c): the third reflector and noninjectivity.) With ρm=3ρ0/2 and θe=0, [L2] gives θm=log⁡(3/2); the hyperbolic values sinh⁡log⁡(3/2)=5/12 and cosh⁡log⁡(3/2)=13/12 give the reflection event qm′′=(3ρ0/2)(5/12,13/12,0,0)=(5ρ0/8,13ρ0/8,0,0), and the return at 2log⁡(3/2) is e+′′=(ρ0sinh⁡(2log⁡(3/2)),ρ0cosh⁡(2log⁡(3/2)),0,0)=(65ρ0/72,97ρ0/72,0,0), using sinh⁡(2u)=2sinh⁡ucosh⁡u=65/72 and cosh⁡(2u)=cosh⁡2u+sinh⁡2u=97/72 at u=log⁡(3/2) by [L4]; the radar distance is ρ0log⁡(3/2), the rest distance in the slice is ρ0/2 by [L3] (the same as in step 2.1), and ρ0log⁡(3/2)<ρ0log⁡2 because 3/2<2 and log⁡ is strictly increasing by [L4]. Thus two distinct reflector radii (ρ0/2 and 3ρ0/2) share the rest distance ρ0/2 but have different radar distances, and the two cases of steps 1.1 and 2.1 share the radar distance ρ0log⁡2 at rest distances ρ0 and ρ0/2.

4.1L1L2step 1.1step 2.1step 3.1∎

(Midpoint identities, round-trip times and scope.) In each of the three cases the reported θm is the midpoint (θe+θ(e+))/2 by [L2], and the round-trip proper time of O is ρ0(θ(e+)−θe)/c, equal to 2ρ0log⁡2/c in cases (a) and (b) and to 2ρ0log⁡(3/2)/c 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

Dependency tree · 2 levels

Sources