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.
Local frame formula for covariant differentiation along a curve
Statement
If and , then Thus is the linear system .
Facts & Assumptions
Given: A frame on a neighbourhood of the image of a curve segment and the displayed coefficient column.
The along-curve derivative is intrinsic pullback differentiation (Covariant derivative along a curve is independent of frame and extension).
The pullback connection has matrix obtained by evaluating the original one-forms on the differential of the map (Pullback connection).
Frame changes obey the inhomogeneous matrix transformation law (Connection one form transformation law).
Proof
Apply the pullback prescription to : its action on is and the pulled-back one-form evaluated on is . This gives the formula, and the frame is a basis, so zero covariant derivative is equivalent to .
Explicitly, for a second frame put , write , and use for the new connection matrix (here the prime on denotes the new matrix). Then . Multiplication by the respective frames gives the same derivative. This computation allows singular curve velocity, including zero velocity, and uses no inverse of . Rank zero means empty vectors; rank one is the scalar equation. Endpoint derivatives are one-sided, so the same product rule applies.