Alphabeta Math
PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-12
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.1F1F2

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.

2.1F3step 1.1∎

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

Depends on

Dependency tree · 2 levels

Sources