Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

The uniformly accelerated worldline: hyperbolic motion, constant four-acceleration magnitude, and identification as a Rindler flow line

Statement

Let c>0 and α>0, set R:=c2/α, and let (A,V,η,C+) be the affine Minkowski space with an inertial chart χ=(x0,x1,x2,x3), x0=ct (Oriented time-oriented affine Minkowski space (the spacetime primitives), Inertial frames and inertial charts of the affine Minkowski model). Write xa(τ):=χa(x(τ)) for the coordinate components of the curve x:R→A defined by x(τ):=χ−1(Rsinh⁡θ,Rcosh⁡θ,0,0), where θ:=ατ/c.

(a) Regularity, causal character and parametrization. x is C∞, and x′(τ)=c(cosh⁡θ,sinh⁡θ,0,0) is future timelike for every τ (Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones), so x is a future timelike worldline (Curves, regular causal curves and future timelike worldlines in affine Minkowski space). Since η(x′,x′)=−c2 is constant, the parameter τ is a proper-time parameter of the curve: the proper-time function T of Proper time along a future timelike worldline satisfies T(b)−T(a)=b−a for all a<b in R (Proper time along a future timelike worldline, The proper-time function is a strictly increasing C^1 parametrization with C^1 inverse), and the four-velocity is U:=dx/dτ=c(cosh⁡θ,sinh⁡θ,0,0) with η(U,U)=−c2 (Four-velocity and four-acceleration of a future timelike worldline, Norms of four-velocity and four-acceleration, and the observer rest-space decomposition (a)).

(b) Constant four-acceleration magnitude. The four-acceleration A:=dU/dτ=α(sinh⁡θ,cosh⁡θ,0,0) satisfies η(A,A)=α2 and η(U,A)=0. The chart coordinate velocity is dx1/dt=ctanh⁡θ, so ∣dx1/dt∣<c for every τ, and x1=Rcosh⁡θ>R∣sinh⁡θ∣=∣x0∣ for every τ: the worldline lies in the right wedge W:={x1>∣x0∣} and its speed in the chart tends to c only as τ→±∞.

(c) Rindler flow line. Let Φ(θ,ρ,y,z):=χ−1(ρsinh⁡θ,ρcosh⁡θ,y,z) on R×(0,∞)×R2 and let n:=ρ−1∂θ be the Rindler congruence of Fermi-Walker transport preserves the metric, and explicit rigid and non-rigid observer congruences (b), whose pullback metric is −ρ2dθ2+dρ2+dy2+dz2 and whose congruence acceleration acg:=∇nn is ρ−1∂ρ, with η(acg,acg)=ρ−2 (The flat covariant derivative on affine Minkowski space and fields along curves, Kinematics of an observer congruence: acceleration, expansion, shear, vorticity and Born rigidity). Then x is exactly the flow line Φ(⋅,R,0,0) reparametrized by θ=ατ/c, and along x one has A=c2acg: the four-acceleration of the worldline is c2 times the congruence acceleration, and η(acg,acg)=1/R2=α2/c4 on the flow line ρ=R.

(d) Asymptotic behaviour. Along x one has x1−x0=Re−θ→0 with x0→+∞ as τ→+∞, and x1+x0=Reθ→0 with x0→−∞ as τ→−∞: the worldline approaches each of the null planes {x1=x0} and {x1=−x0} asymptotically without meeting either, and the chart coordinate speed tends to c at both ends.

(e) Scope. This is an exact kinematic computation in the affine model. It uses no force law, no mass, no clock hypothesis and no empirical input; beyond identifying the displayed parameter with the proper time of the curve, only the flow parametrization of the congruence is used. The curve is not asserted to be a geodesic and no statement is made about the forces that would maintain it. No choice principle is used.

Facts & Assumptions

Given: The affine Minkowski space (A,V,η,C+) with fixed c>0; an inertial chart χ=(x0,x1,x2,x3) with x0=ct and orthonormal basis (e0,e1,e2,e3) (Inertial frames and inertial charts of the affine Minkowski model); α>0, R=c2/α, θ=ατ/c, and the curve x(τ)=χ−1(Rsinh⁡θ,Rcosh⁡θ,0,0) for τ∈R.

[L1]

Model and chart: χ(p)=E−1(p−o) for the frame isomorphism E, so specifying the four coordinates determines the event, and vector components are read in the orthonormal basis (ea) in which η has matrix diag⁡(−1,1,1,1) (Oriented time-oriented affine Minkowski space (the spacetime primitives), Inertial frames and inertial charts of the affine Minkowski model).

[L2]

Differentiability of a curve x:I→A is defined through its coordinate representation χ∘x, with x′(τ)=E((χ∘x)′(τ)); the curve is Ck when the coordinate map is (Curves, regular causal curves and future timelike worldlines in affine Minkowski space (a)).

[L3]

sinh⁡u=(eu−e−u)/2, cosh⁡u=(eu+e−u)/2, tanh⁡u=sinh⁡u/cosh⁡u, and cosh⁡u>0 for all real u (The six hyperbolic functions and their natural domains).

[L4]

cosh⁡2u−sinh⁡2u=1, (sinh⁡u)′=cosh⁡u, (cosh⁡u)′=sinh⁡u, sinh⁡ is odd, cosh⁡ is even, tanh⁡:R→(−1,1) is strictly increasing and onto (Addition formulas, identities, parity, and derivatives of the hyperbolic functions). The limits tanh⁡u→±1 follow from its exponential formula and [L14].

[L6]

Coordinate criterion: in any inertial chart, C+={v:v0>∣vs∣} and Cˉ+={v:v0≥∣vs∣}, where v0 is the time component and ∣vs∣ the Euclidean norm of the spatial part (The closed future cone in inertial coordinates: description, finite sums, and the coordinate criterion for causal reachability (a)).

[L7]

Causal classification: a vector v is timelike if η(v,v)<0, spacelike if η(v,v)>0, and each nonzero timelike vector is future or past but not both (Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones).

[L8]

Proper time: for a C1 future timelike worldline x, τ(b)−τ(a)=c−1∫ab−η(x′(u),x′(u)) du, defined up to an additive constant (Proper time along a future timelike worldline).

[L9]

Proper-time parametrization: τ is C1 and strictly increasing with τ′(s)=c−1−η(x′(s),x′(s))>0; the reparametrized curve x∘ρ has tangent x′(s)/τ′(s) at the proper-time parameter, and the derivative formula is the four-velocity (The proper-time function is a strictly increasing C^1 parametrization with C^1 inverse (i),(iii),(iv)).

[L10]

Four-velocity and four-acceleration: U=x′/τ′=cx′/−η(x′,x′), and for C2 curves A=U′/τ′ is the derivative of U with respect to the proper-time parameter (Four-velocity and four-acceleration of a future timelike worldline (a),(b)); η(U,U)=−c2 and η(U,A)=0 with A spacelike wherever it is nonzero (Norms of four-velocity and four-acceleration, and the observer rest-space decomposition (a),(b)).

[L11]

The smooth Rindler field of [L13] is future unit timelike; its acceleration is acg=∇nn with η(n,acg)=0 (Kinematics of an observer congruence: acceleration, expansion, shear, vorticity and Born rigidity (b),(e)).

[L12]

Covariant derivative along curves: for a C1 curve y and a C1 ambient field W defined near its image, the derivative of the restricted field W∘y is ∇y˙W in the canonical identification, and ∇fXY=f∇XY (The flat covariant derivative on affine Minkowski space and fields along curves (a),(d)).

[L13]

Rindler congruence: Φ(θ,ρ,y,z)=χ−1(ρsinh⁡θ,ρcosh⁡θ,y,z) is a smooth bijection onto the right wedge W with pullback metric −ρ2dθ2+dρ2+dy2+dz2; n=ρ−1∂θ is future unit timelike, Born rigid and irrotational, with acg=ρ−1∂ρ and η(acg,acg)=ρ−2 (Fermi-Walker transport preserves the metric, and explicit rigid and non-rigid observer congruences (b)).

[L14]

Exponential limits: eu→+∞ as u→+∞ and eu→0 as u→−∞ (The exponential tends to +∞ at +∞ and to 0 at −∞).

Proof

technique · direct
1.1L1L2L3L4L5algebra

(The tangent.) Writing x in the chart, the coordinate functions are τ↦Rsinh⁡(ατ/c), τ↦Rcosh⁡(ατ/c), and the two constants 0; differentiating with the chain rule and the hyperbolic derivative formulas gives x′(τ)=(Rαccosh⁡θ, Rαcsinh⁡θ, 0, 0)=(ccosh⁡θ, csinh⁡θ, 0, 0), because Rα/c=c by R=c2/α. In particular the coordinate functions are C∞, since each derivative has the same form with sinh⁡ and cosh⁡ exchanged.

1.2L3L4algebra

(Elementary hyperbolic identities.) From the exponential definitions, cosh⁡θ−sinh⁡θ=e−θ and cosh⁡θ+sinh⁡θ=eθ; combined with cosh⁡2θ−sinh⁡2θ=1 and cosh⁡θ>0 this gives cosh⁡θ>∣sinh⁡θ∣≥0, hence ∣tanh⁡θ∣<1 for every θ.

1.3L1L13given

(The curve is a Rindler flow line.) Substituting ρ=R, y=z=0 into Φ gives Φ(θ,R,0,0)=χ−1(Rsinh⁡θ,Rcosh⁡θ,0,0)=x(τ) with θ=ατ/c; hence x is exactly the flow line Φ(⋅,R,0,0), reparametrized by the affine map τ↦θ=ατ/c, and at ρ=R the Rindler field is n=R−1∂θ with acceleration acg=R−1∂ρ.

2.1L6L7step 1.1step 1.2

(x is a C∞ regular future timelike worldline.) By step 1.1 the coordinate functions are C∞, so x is C∞ by [L2]; η(x′,x′)=c2(−cosh⁡2θ+sinh⁡2θ)=−c2<0 by step 1.2 and the matrix of η in the frame, so x′ is timelike; and its time component is x′0=ccosh⁡θ>c∣sinh⁡θ∣=∣(x′)s∣ by step 1.2, so x′∈C+ by the coordinate criterion [L6]. Hence x′ is future timelike and nonzero, and x is a future timelike worldline.

2.2L1L3step 1.1step 1.2

(Chart speed and the wedge.) The chart time is x0=ct with x′0=ccosh⁡θ, so dt/dτ=cosh⁡θ and, by step 1.1, dx1/dt=(dx1/dτ)/(dt/dτ)=csinh⁡θ/cosh⁡θ=ctanh⁡θ; step 1.2 gives ∣dx1/dt∣=c∣tanh⁡θ∣<c. Also x1=Rcosh⁡θ>R∣sinh⁡θ∣=∣x0∣ by step 1.2, so the worldline lies in W={x1>∣x0∣}.

3.1L8L9L10step 1.1step 2.1

(Proper-time parametrization and four-velocity.) By step 2.1 the curve is a C1 future timelike worldline, so its proper-time function satisfies T(b)−T(a)=c−1∫ab−η(x′,x′) du=c−1∫abc du=b−a by [L8] and step 2.1; thus the given parameter is a proper-time parameter of x up to an additive constant, in agreement with [L9]. Consequently the four-velocity is U=x′/T′=c(cosh⁡θ,sinh⁡θ,0,0) by [L10] and step 1.1, and η(U,U)=−c2.

3.2L4L14step 1.2step 2.2

(Asymptotics.) From the addition formulas in exponential form of step 1.2, x1−x0=R(cosh⁡θ−sinh⁡θ)=Re−θ and x1+x0=R(cosh⁡θ+sinh⁡θ)=Reθ, both strictly positive for every τ. As τ→+∞ we have θ→+∞, so e−θ→0 by [L14] and x0=Rsinh⁡θ→+∞; as τ→−∞ we have θ→−∞, so eθ→0 and x0→−∞. Hence the worldline approaches both null planes asymptotically and meets neither. For θ→+∞, tanh⁡θ=(1−e−2θ)/(1+e−2θ)→1 by [L14]; oddness gives the negative-end limit −1. Thus the signed chart velocity tends to ±c and its magnitude to c.

4.1L4L5L10step 1.2step 3.1algebra

(The four-acceleration and its magnitude.) Differentiating each component of U in the proper-time parameter τ with the chain rule and the hyperbolic derivative formulas gives A=U′=c(sinh⁡θ,cosh⁡θ,0,0)αc=α(sinh⁡θ,cosh⁡θ,0,0). Then η(A,A)=α2(−sinh⁡2θ+cosh⁡2θ)=α2 and η(U,A)=cα(−cosh⁡θsinh⁡θ+sinh⁡θcosh⁡θ)=0 by step 1.2; the second identity is consistent with [L10].

4.2L11L12L13step 1.3step 3.1

(Identification of the four-acceleration with c2acg.) Along x one has dx/dτ=cn by steps 1.3 and 3.1 with n=R−1∂θ; the total derivative of n∘x along this smooth curve is ∇dx/dτn, and by [L12] and [L11] it equals ∇cnn=c∇nn=cacg. Therefore A=dU/dτ=c d(n∘x)/dτ=c∇dx/dτn=c2acg. Substituting ρ=R into η(acg,acg)=ρ−2 from [L13] gives η(acg,acg)=1/R2=α2/c4.

5.1L11step 3.1step 3.2step 4.1step 4.2∎

(Scope.) Every step above is a finite-dimensional computation in the affine model from the cited definitional suppliers: the curve, its causal character, its proper-time parametrization, its four-acceleration, the identification A=c2acg and the asymptotics. No force law, mass, geodesic property, clock hypothesis or empirical input was used, and no choice principle was used.

Depends on

Dependency tree · 2 levels

Sources