Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generated
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 and rigid rotating bath domains

Physical scope

Rindler right wedge and rigidly rotating Minkowski domain inside its light cylinder; arbitrary positive classical reference temperature; differential rotation and one-mode trace restrictions kept distinct.

Example

Rindler right wedge. Let a0>0 be an acceleration in m s−2, use coordinates (x0,x,y,z) with x0=ct, and take the open domain x>0 with metric

ds2=−(a0xc2)2(dx0)2+dx2+dy2+dz2.

The selected Killing field ξR=∂x0 has lapse NR=a0x/c2 and observer acceleration ax=1/x, so the physical proper-acceleration magnitude is c2/x. The selected stationary-bath model gives

TR(x)=TKc2a0x.

At the reference point xref=c2/a0, NR=1 and TR=TK. Any TK>0 is allowed by this classical geometric model; the metric and temperature relation do not select the Unruh value.

Rigid rotation in Minkowski spacetime. In cylindrical coordinates let

ds2=−(dx0)2+dr2+r2dϕ2+dz2,ξΩ=∂x0+Ωc∂ϕ,

where Ω is a constant angular velocity in s−1. For Ω≠0, use the annular domain 0<r<c/∣Ω∣; for Ω=0, ξΩ=∂x0 is timelike throughout Minkowski space. On the rotating domain,

NΩ=1−Ω2r2c2,TΩ(r)=TKNΩ.

The radial acceleration component is ar=−Ω2r/[c2(1−Ω2r2/c2)], directed inward, with physical magnitude γ2Ω2r, where γ=(1−Ω2r2/c2)−1/2. At the light cylinder r=c/∣Ω∣, ξΩ becomes null and the normalized stationary observer does not exist. A differential-rotation field ∂x0+[Ω(r)/c]∂ϕ is not Killing when Ω′(r)≠0: its metric Lie derivative has (Lξg)rϕ=r2Ω′(r)/c.

One-mode trace check. If an additional model specifies a single bosonic mode with lab Hamiltonian H=ϵN and angular momentum J=ℏjN, then its rotating generator is H−ΩJ. Its Gibbs trace is finite exactly when ϵ−ℏjΩ>0. This is the separate one-mode spectral condition of Rotating mode Gibbs obstruction; it does not prove a continuum-field trace obstruction or describe every rotating equilibrium state.

Domain sketches

The left panel uses dimensionless Minkowski coordinates (X/ℓ,X0/ℓ) for a fixed length ℓ>0 and the exact Rindler embedding

X=xcosh⁡(a0x0/c2),X0=xsinh⁡(a0x0/c2).

It maps x>0 onto the right wedge X>∣X0∣; the red curve is the constant-Rindler-position orbit x=ℓ, which obeys X2−(X0)2=ℓ2. The right panel is a fixed-z cross-section of the Ω≠0 rotating timelike domain. Its dashed circle is the excluded null boundary r=c/∣Ω∣, and the shaded open disk is where g(ξΩ,ξΩ)<0. The sketches show domains only; every lapse, acceleration, and temperature claim is established by the coordinate calculations in Verification.

RindlerrightwedgeX=`X0=`rightwedgex=`X=X0X=¡X0Rigidrotationat¯xedzXYc=j¬jtimelikenullboundary

Facts & Assumptions

Given: The displayed Rindler and Minkowski metrics, the constant parameters a0>0 and Ω, and a selected stationary bath only where its stated Killing field is future timelike.

[F1]

Conditional Tolman–Ehrenfest relation: on a selected connected stationary bath, NξT=TK and a=∇log⁡Nξ for the chosen future timelike Killing field. Its physical conclusion is conditional on the postulated bath, not a universal thermometer law.

[F2]

Rotating mode Gibbs obstruction: for a single bosonic occupation mode with ϵ>0, integer mode number, Ω in s−1, and positive inverse temperature, the diagonal partition sum is finite exactly when ϵ−ℏjΩ>0. The proposition explicitly constructs no continuum field state.

[A1]

The Rindler metric and the rotating Minkowski metric are the exact model geometries used in this example; ξR and ξΩ are the explicitly selected Killing generators on their respective timelike domains.

[A2]

The Rindler and rotating temperature fields are conditional classical bath assumptions. No equilibrium state is constructed, and no Unruh or Hawking temperature is inferred.

[A3]

The one-mode trace paragraph applies only when the additional Hamiltonian and angular-momentum assignments displayed in the Example are adopted.

Verification

technique · Compute the lapse and acceleration in each exact geometry, apply the conditional Tolman relation, and keep the single-mode trace premise separate
1.1givenA1algebra

The Rindler metric is independent of x0, so ξR is Killing. Its norm is g(ξR,ξR)=−(a0x/c2)2<0 on x>0, hence NR=a0x/c2. Differentiating log⁡NR gives ax=1/x, whose metric norm is 1/x.

1.2givenA1algebra

In the rotating Minkowski metric, ∂x0 and ∂ϕ are Killing fields and Ω is constant, so their displayed linear combination ξΩ is Killing. Its squared norm is −1+Ω2r2/c2, which is negative exactly for r<c/∣Ω∣ when Ω≠0; therefore NΩ=1−Ω2r2/c2.

1.3givenalgebra

For a nonconstant angular velocity, the coordinate formula for the Lie derivative gives (Lξg)rϕ=gϕϕ∂r(Ω/c)=r2Ω′(r)/c. Thus if Ω′(r)≠0, this field is not Killing and the selected stationary theorem does not apply.

2.1F1A2step 1.1algebra

By [F1] and [A2], the selected Rindler bath has TR=TK/NR=TKc2/(a0x) and physical proper acceleration c2∣a∣=c2/x. The point xref=c2/a0 has NR=1, so it provides the stated reference normalization.

2.2F1step 1.2algebra

Applying [F1] on that selected timelike domain yields TΩ=TK/NΩ. Differentiating log⁡NΩ gives ar=−Ω2r/[c2(1−Ω2r2/c2)]. Since grr=1, its physical magnitude is c2∣ar∣=γ2Ω2r. At the light cylinder the norm tends to zero and the timelike-field hypothesis of [F1] fails.

3.1F2A3step 1.2∎

Under [A3], the mode generator has coefficient a=ϵ−ℏjΩ in the exact occupation model of [F2]. Applying [F2] gives a finite trace exactly for a>0. This condition is logically separate from the geometric timelike-domain condition in step 1.2 and supplies no continuum-field conclusion.

Depends on

Dependency tree · 2 levels

Sources