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 and the smooth fields be as in Stationary thermal geometric data. Then When this holds, , and the Killing congruence has If is replaced by with a constant , then and scale by , while and are unchanged.
Facts & Assumptions
Given: The connected open domain and smooth stationary carrier fields of Stationary thermal geometric data.
The definition supplies , , , , and the Killing equation ; 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).
On a real interval, a differentiable function with zero derivative is constant by the mean value theorem (The mean value theorem, as the case of Cauchy's: for continuous on with and differentiable on there is with ).
For the unit convention here, use length coordinates (including ), a length-valued local flow parameter for , and dimensionless metric components. Then the coordinate components of and are dimensionless, has kelvin units, and the constant rescaling factor in the Statement is dimensionless.
Proof
Differentiating with the metric-compatible connection gives , since by the Killing equation. The same equation gives . Therefore . Also because and . The symmetric derivative is ; projecting both indices with gives zero, so .
Put , so . If is Killing, both and have zero symmetric covariant derivative, and hence . Contracting with gives because and ; contracting with gives . The decomposition of a covector into its and rest-space parts now gives .
In a convex coordinate ball in , join any two coordinate points by a straight segment. The derivative of along that segment is zero by the covector decomposition just proved, so [F2] makes constant on the ball. Thus is locally constant on . Each level set of and its complement are open; connectedness of therefore makes one positive constant. Equivalently for a constant , and then .
Conversely, if is constant, then is a constant multiple of the Killing field and is Killing. Under , and , whereas and remain fixed. These identities prove the converse and the normalization statement.
Depends on
Dependency tree · 2 levels
Sources
- José Santiago and Matt Visser, Tolman-like temperature gradients in stationary spacetimes, §§III–V
- Rubén O. Acuña-Cárdenas, Carlos Gabarrete, and Olivier Sarbach, An introduction to the relativistic kinetic theory on curved spacetimes, §VI.2
- David Tong, General Relativity, full Cambridge Part III lecture notes, §§2.2.3 and 4.3.1