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

Exact thermal Killing kinematic equivalence

Statement

Let O be a connected open set in a smooth time-oriented Lorentzian four-manifold, let u be a smooth future unit timelike vector field on O (g(u,u)=−1), and let T:O→(0,∞) be smooth. Define β:=u/(kBT), hab:=gab+uaub, D:=ua∇a, ab:=ua∇aub, θ:=∇aua and σab:=hachbd∇(cud)−θhab/3 as in Stationary thermal geometric data. Then β is a Killing field of g (equivalently ∇(aβb)=0 by Killing fields of a Lorentzian metric and Killing fields and conserved currents, and on-shell conservation of the Hilbert stress-energy tensor) if and only if DT=0,θ=0,σab=0,hab∇blog⁡T=−aa. No hypersurface-orthogonality or vanishing-vorticity condition is assumed.

Facts & Assumptions

Given: A smooth future unit timelike field u, a positive smooth scalar T, and the metric-selected connection and kinematic definitions of Stationary thermal geometric data.

[F1]

The connection is torsion-free and metric-compatible, and the definitions give uaua=−1, uaaa=0, and hab=δab+uaub (Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields, Stationary thermal geometric data). Killing means Lβg=0, equivalently ∇(aβb)=0 (Killing fields of a Lorentzian metric, Killing fields and conserved currents, and on-shell conservation of the Hilbert stress-energy tensor).

Proof

1.1givenF1algebra

Differentiating ubub=−1 gives ub∇aub=0. Decompose the first derivative slot into its component parallel to u and its rest-space projection: ∇aub=−uaab+hachbd∇cud. Symmetrizing the rest-space term and using the definitions of expansion and shear yields ∇(aub)=−u(aab)+σab+θhab/3. Differentiating β=u/(kBT) then gives ∇(aβb)=(kBT)−1[−u(a(ab)+∇b)log⁡T)+σab+13θhab].

2.1step 1.1algebra

Contracting this identity with uaub shows that ∇(aβb)=0 implies Dlog⁡T=0, hence DT=0 because T>0.

2.2step 1.1algebra

Projecting both indices with h gives σab+13θhab=0. Taking its h-trace gives θ=0, since h has rank three and σ is trace-free; substituting back gives σab=0.

2.3step 1.1algebra

Contracting one index with u and projecting the other with h gives hab(ab+∇blog⁡T)=0. Thus the displayed temperature-gradient condition also follows from the Killing equation.

3.1step 1.1step 2.1step 2.2step 2.3algebra∎

Conversely, the four stated conditions make the parallel, mixed and rest-space projections in step 1.1 all zero. Since TxM=span⁡{ux}⊕ux⊥ at every x∈O, these projections determine the full symmetric tensor ∇(aβb); it is zero, so β is Killing. In particular, the acceleration/temperature-gradient relation alone omits the necessary conditions DT=0, θ=0 and σ=0.

Depends on

Dependency tree · 2 levels

Sources