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.

Killing temperature normalization and rigidity

Statement

Let O and the smooth fields (g,∇,ξ,T,u,Nξ,β) be as in Stationary thermal geometric data. Then β is Killing⟺NξT=TK for a constant TK>0. When this holds, β=ξ/(kBTK), and the Killing congruence has ξ(Nξ)=0,a=∇log⁡Nξ,θ=0,σab=0. If ξ is replaced by bξ with a constant b>0, then Nξ and TK scale by b, while u and β are unchanged.

Facts & Assumptions

Given: The connected open domain and smooth stationary carrier fields of Stationary thermal geometric data.

[F1]

The definition supplies Nξ=−g(ξ,ξ)>0, u=ξ/Nξ, g(u,u)=−1, β=u/(kBT), and the Killing equation ∇(aξb)=0; ∇ is torsion-free and metric-compatible (Stationary thermal geometric data, Existence and uniqueness of the metric-selected connection of a nondegenerate metric, and its extension to tensor fields).

[F3]

For the unit convention here, use length coordinates (including x0=ct), a length-valued local flow parameter for ξ, and dimensionless metric components. Then the coordinate components of ξ and Nξ are dimensionless, TK=NξT has kelvin units, and the constant rescaling factor b>0 in the Statement is dimensionless.

Proof

1.1givenF1algebra

Differentiating g(ξ,ξ) with the metric-compatible connection gives ξ(Nξ)=0, since ξaξb∇aξb=0 by the Killing equation. The same equation gives ξa∇aξb=−12∇bg(ξ,ξ)=Nξ∇bNξ. Therefore ab=ua∇aub=∇blog⁡Nξ. Also θ=∇a(ξa/Nξ)=0 because ∇aξa=0 and ξ(Nξ)=0. The symmetric derivative is ∇(aub)=−u(a∇b)log⁡Nξ; projecting both indices with h gives zero, so σab=0.

1.2givenF1algebra

Put f:=(kBNξT)−1>0, so β=fξ. If β is Killing, both fξ and ξ have zero symmetric covariant derivative, and hence ξ(b∇a)f=0. Contracting with uaub gives u(f)=0 because ξ=Nξu and Nξ>0; contracting with uahbc gives hbc∇bf=0. The decomposition of a covector into its u and rest-space parts now gives df=0.

2.1step 1.2F2algebra

In a convex coordinate ball in O, join any two coordinate points by a straight segment. The derivative of f along that segment is zero by the covector decomposition just proved, so [F2] makes f constant on the ball. Thus f is locally constant on O. Each level set of f and its complement are open; connectedness of O therefore makes f one positive constant. Equivalently NξT=TK for a constant TK>0, and then β=ξ/(kBTK).

3.1step 2.1F1algebra∎

Conversely, if NξT=TK is constant, then β=ξ/(kBTK) is a constant multiple of the Killing field ξ and is Killing. Under ξ↦bξ, Nξ↦bNξ and TK↦bTK, whereas u=ξ/Nξ and β=ξ/(kBTK) remain fixed. These identities prove the converse and the normalization statement.

Depends on

Dependency tree · 2 levels

Sources