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

Ricci contraction of the Killing derivative

Statement

For stationary Lorentzian data, the Killing two-form obeys ∇aFab=−Ric⁡bdTd. In particular, if Ric⁡=0, then ∇aFab=0. The curvature and Ricci signs are those of the stationary-data definition.

Facts & Assumptions

[F1]

The connection, index conventions, curvature and Ricci contraction are those of Stationary Lorentzian data and tensor conventions.

[F2]

The Killing derivative is alternating. The Killing derivative is an exact closed two-form

[F3]

The curvature has the pair skew-symmetries, pair-exchange symmetry and symmetric Ricci contraction. The algebraic symmetries of the curvature tensor and the symmetry of the Ricci and Einstein tensors

[F4]

Import the vector Ricci commutator with the exact convention recorded in the External input; its source is Reall (4.7)–(4.8).

Proof

Given: The data and hypotheses in the Statement.

Goal: Prove all asserted identities under these hypotheses.

1.1F1F3F4algebra

Apply the commutator in [F4] to the scalar pairing ucZc and use the connection product rule. Scalar second derivatives commute by torsion freedom, so the covector formula is [∇a,∇b]uc=−Rdcabud. Contracting u=T♭ gives gac[∇a,∇b]Tc=Ric⁡bdTd: indeed gacRecab=−gacRceab=−Ric⁡eb, using the first-pair skew-symmetry and the stated Ricci contraction.

2.1step 1.1F1F2algebra∎

Alternation gives ∇aTa=0 and ∇aFab=−∇a∇bTa. Metric compatibility and step 1.1 therefore yield ∇aFab=−∇b(∇aTa)−gac[∇a,∇b]Tc=−Ric⁡bdTd. Under Ricci flatness the right side vanishes.

External input

The vector identity [∇c,∇d]Za=RabcdZb and contraction Ric⁡ab=Rcacb are the imported input from Reall (4.7)–(4.8). Its convention matches the stationary-data definition exactly. No sign of a curvature tensor from a different source is transferred implicitly.

Depends on

Used by · 2

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

External dependencies

H. S. Reall, General Relativity, Part III Mathematical Tripos, October 12, 2022 · Conventions, printed p. 3 (PDF p. 4); §4.2, equations (4.7)–(4.8), printed p. 42 (PDF p. 43)

For a torsion-free connection, $(\nabla_c\nabla_d-\nabla_d\nabla_c)Z^a=R^a{}_{bcd}Z^b$. The Ricci contraction is $R_{ab}=R^c{}_{acb}$.

Hypotheses: A smooth torsion-free connection and a smooth vector field; the curvature convention is the one explicitly stated in the cited Conventions.

Reading limits: Retrieved the PDF and read the Conventions and the §4.2 passage containing (4.7)–(4.8). Equation (4.8) is stated as an exercise with a hint; no complete source proof was read. The identity is explicitly imported here; dualization and its Killing-field application are authored locally. No full-text proof review is claimed.

Sources