Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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 variation formula for length

Statement

Let α:(−ε,ε)×[a,b]→M be a piecewise smooth variation with common subdivision a=t0<⋯<tm=b and regular central curve γ=α(0,⋅), meaning that each one-sided velocity T=γ˙ on each closed smooth piece is nonzero. Put U=T/∣T∣g on each piece and V=∂sα(0,⋅). Then dds∣s=0L(γs)=g(V(b),U(b−))−g(V(a),U(a+))−∑j=1m−1g(V(tj),U(tj+)−U(tj−))−∑j=1m∫tj−1tjg(V,DtU) dt. For a smooth regular curve the corner sum is empty. Fixed endpoints remove the two outer boundary terms.

Facts & Assumptions

Given: The variation and regular central curve in the statement, with a<b.

[F1]

Smooth variation and variation field of a curve supplies stripwise smoothness and a continuous variation field, while Riemannian speed and length expresses length as the finite sum of speed integrals.

[F2]

Fundamental theorem of riemannian geometry supplies the unique Levi--Civita connection. Its metric compatibility is the product rule in Levi civita connection and Metric compatible connection on a riemannian vector bundle, and its torsion freeness is the coordinate symmetry in Torsion free is equivalent to symmetric christoffel symbols in coordinate frames. Covariant derivative along a curve fixes the stripwise and one-sided meanings of Dt.

[F4]

First variation formula for energy gives the corresponding half-energy formula, including its endpoint and corner signs.

Proof

technique · direct
1.1F1F3given

On each closed central piece, ∣T∣g is continuous and positive, so [F3] gives a positive minimum. Continuity of g(∂tα,∂tα) on a small compact parameter rectangle and uniform continuity in [F3] then give a common δ>0 such that ∂tα(s,t)≠0 on every strip whenever ∣s∣≤δ. Thus the speed is smooth there and differentiation under its integral is legitimate.

2.1F1F2F3step 1.1

Metric compatibility and the derivative of the positive square root give ∂s∣0∣∂tα∣g=g(Ds∂tα,T)∣T∣g=g(Ds∂tα,U). In local coordinates, equality of mixed partials and the symmetric lower Christoffel indices in [F2] give Ds∂tα=Dt∂sα. Hence [F3] yields dds∣0L(γs)=∑j=1m∫tj−1tjg(DtV,U) dt.

3.1F1F2F3step 2.1

On each smooth piece, metric compatibility says g(DtV,U)=ddtg(V,U)−g(V,DtU). Newton--Leibniz from [F3] therefore turns step 2.1 into the sum of g(V(tj),U(tj−))−g(V(tj−1),U(tj−1+)) minus the displayed integrals of g(V,DtU).

4.1F1F4step 3.1

Continuity of V telescopes the interior boundary values to −g(V(tj),U(tj+)−U(tj−)), while the two surviving outer terms have the signs stated. If m=1 the corner sum is empty; if endpoints are fixed, [F1] gives V(a)=V(b)=0. When ∣T∣g=1 on every piece, U=T, so this formula agrees term by term with [F4].

5.1F1F2F3step 1.1step 2.1step 3.1step 4.1∎

Regularity excludes a constant or zero-length central curve on a<b and excludes all such curves in dimension zero; those are genuinely outside the theorem rather than hidden divisions by zero. A zero variation field makes the derivative and all terms zero. Dimension one is unchanged. An empty target admits no given curve. One-sided endpoint and corner velocities are explicit in the statement, and compactness is used only over finitely many supplied strips. The Levi--Civita connection is unique and every compactness argument in [F3] is choice-free, so no choice axiom is used.

Depends on

Used by

Dependency tree · two levels

81 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