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

Local frame formula for covariant differentiation along a curve

Statement

If V(t)=e(γ(t))v(t) and B(t)=ωγ(t)(γ˙(t)), then DtV=e(γ(t))(v(t)+B(t)v(t)). Thus DtV=0 is the linear system v=Bv.

Facts & Assumptions

Given: A frame on a neighbourhood of the image of a curve segment and the displayed coefficient column.

[F1]

The along-curve derivative is intrinsic pullback differentiation (Covariant derivative along a curve is independent of frame and extension).

[F2]

The pullback connection has matrix obtained by evaluating the original one-forms on the differential of the map (Pullback connection).

[F3]

Frame changes obey the inhomogeneous matrix transformation law (Connection one form transformation law).

Proof

1.1

Apply the pullback prescription to X=t: its action on v is v and the pulled-back one-form evaluated on t is B(t). This gives the formula, and the frame is a basis, so zero covariant derivative is equivalent to v+Bv=0.

F1F2
2.1

Explicitly, for a second frame put C(t)=A(γ(t)), write v=Cw, and use B=C1BC+C1C for the new connection matrix (here the prime on B denotes the new matrix). Then v+Bv=Cw+Cw+BCw=C(w+Bw). 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.

F3step 1.1

Depends on

Used by

Dependency tree · two levels

10 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