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 equation for the normal connection
Statement
Assume . Let be the curvature of the normal connection. For tangent fields and normal fields along an embedded Riemannian submanifold,
where . Both curvatures use the bracket-corrected sign convention, and the choice hypothesis is inherited exactly through the smooth normal-bundle projections.
Facts & Assumptions
Given: Countable choice, an embedded Riemannian submanifold, tangent fields , and normal fields .
The Weingarten decomposition is , and shape operators are self-adjoint with . Weingarten equation and adjointness of the shape operator.
The projected operation is a connection on . Normal connection.
The shape operator is pointwise and linear in its normal direction. Shape operator.
The curvature of a vector-bundle connection is . Curvature of a vector-bundle connection.
Proof
Apply [F1] first to . The normal component after differentiating in direction is The analogous formula holds with interchanged, and .
Form the bracket-corrected ambient curvature and take its normal component. By [F4], the three normal-connection terms combine to , leaving
Pair step 2.1 with and use [F1]: the two correction terms become . Self-adjointness rewrites their sum as which proves the stated equation.
The equation is vacuous on the empty submanifold. If tangent or normal rank is zero every term vanishes; in tangent rank one the curvature pair and the commutator vanish. The same calculation applies for a normal line bundle and at boundary points. Positive definiteness supplies the orthogonal splitting and self-adjointness. The stated is inherited through [F1]–[F3], and no new selection occurs.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
12 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
- Chuu-Lian Terng, Lecture Notes on Curves and Surfaces in R^3 and Riemannian Geometry (standard reference, not scraped)