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.
First Bianchi identity
Statement
This item assumes , namely countable choice. In the propagated dependency chain, that assumption is required through Smoothness of a vector field is equivalent to smooth coordinate components; after those interfaces are fixed, the remaining local or finite argument makes no additional countable-family choice.
For the torsion-free Levi–Civita connection and all smooth vector fields ,
Equivalently, the cyclic sum over the three input slots of the curvature endomorphism vanishes.
Facts & Assumptions
is countable choice and is required here through Smoothness of a vector field is equivalent to smooth coordinate components; after those supplied interfaces are fixed, the remaining local or finite calculation makes no additional countable-family choice.
Curvature is the bracket-corrected commutator of covariant derivatives. Curvature of an affine connection.
Torsion freeness of the Levi–Civita connection says . Levi civita connection.
In a chart, smoothness of a vector field is equivalent to smoothness of its coordinate coefficients. Smoothness of a vector field is equivalent to smooth coordinate components.
The Lie bracket is the commutator of the two vector fields acting on smooth functions: . The Lie bracket of smooth vector fields.
Proof
Given: , smooth vector fields and the Levi–Civita connection .
On any coordinate chart, write and . Applying [F4] to a local smooth function and using the ordinary product rule, the terms with second derivatives cancel and give The displayed coefficients are smooth by [F3], so every bracket used below is a smooth vector field.
Expanding the three curvature terms by [F1] and collecting derivatives with the same outer field gives the cyclic sum as By [F2] the three parenthesized differences are , , and .
Acting on an arbitrary local smooth function and using [F4], expand the twelve resulting third-order compositions in Each composition occurs once with sign and once with sign ; hence the sum is zero. Since equality of vector fields is local and is detected by their action on smooth functions, the Jacobi identity holds for .
Apply [F2] once more to pair each term with , and cyclically. The expression from step 1.2 becomes , which is zero by step 2.1.
Depends on
Used by
Dependency tree · two levels
17 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Ved Datar, Lectures on Riemannian Geometry (standard reference, not scraped)
- John M. Lee, Riemannian Manifolds: An Introduction to Curvature (standard reference, not scraped)