Alphabeta Math
PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passverified 2026-09-26 (gpt-6-sol)
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 of volume for a normal variation

Statement

Assume ACω. Let Mm be a smooth manifold of dimension m≥1, let (M‾,g‾) be Riemannian, and let

F:(−ε,ε)×M⟶M‾

be smooth with every Ft:=F(t,⋅) an immersion. Put f=F0, gt=Ft∗g‾, and V(p)=dF(0,p)(∂t). Suppose that V is normal to df(TM) and has compact support. If K⊆M is a compact smooth domain satisfying supp⁡V⊆int⁡MK, define

AK(t):=Vol⁡gt(K)=∫Kμgt.

Then, for the averaged mean-curvature vector Hf,

AK′(0)=−m∫Kg‾(V,Hf) μg=−m∫Mg‾(V,Hf) μg.

The derivative is independent of the eligible domain K. If M is compact, one may take K=M, obtaining the first variation of total volume. The choice hypothesis is inherited exactly through the normal projections and density integration.

If M is boundaryless, the same integral formula holds without the normality hypothesis on V: since Hf is normal, the integrand automatically sees only V⊥. Thus in the boundaryless case vanishing mean curvature implies stationarity under every compactly supported variation, not merely the normal ones.

Facts & Assumptions

Given: Countable choice, the stated smooth family of immersions, normal compactly supported variation field V, and eligible compact domain K.

[F1]

The immersion normal bundle and second fundamental form are well defined, and mHf=tr⁡gIIf. Mean curvature vector.

[F2]

Each pullback gt=Ft∗g‾ is a smooth positive-definite metric because Ft is an immersion. Pullback of a riemannian metric is riemannian exactly for immersions.

[F3]

In coordinates the Riemannian density is det⁡G(t)∣dx1⋯dxm∣. Riemannian volume density.

[F4]

On the invertible locus, Jacobi's formula is Ddet⁡(G)[G˙]=det⁡(G)tr⁡(G−1G˙). The determinant differential is Ddet⁡(A)[H]=tr⁡(adj⁡(A)H) at every matrix, and Jacobi's formula holds on the invertible locus.

[F5]

The ambient Levi–Civita connection is metric compatible and torsion free; in coordinate frames the latter is symmetry of the Christoffel symbols. Levi civita connection, Torsion free is equivalent to symmetric christoffel symbols in coordinate frames.

[F6]

Every immersion is locally an embedding, and on each such neighbourhood the Weingarten identity gives g‾(∇‾XV,df(Y))=−g‾(V,IIf(X,Y)) for normal V. Every immersion is locally an embedding, Weingarten equation and adjointness of the shape operator.

[F7]

A parameter derivative dominated by one integrable function may pass through an integral. Differentiation under the integral sign.

[F8]

Under countable choice, compactly supported smooth Riemannian densities have intrinsic, orientation-free integrals, including on manifolds with boundary. Riemannian volume of a compactly supported smooth density.

[F9]

On a boundaryless smooth manifold, a compactly supported smooth tangent field is complete, and its time maps are diffeomorphisms with inverse time maps. Compactly supported smooth vector fields are complete, Time-t flow maps are diffeomorphisms between open domains.

[F10]

Intrinsic density integration is invariant under diffeomorphisms. Orientation-free density integration and its properties.

Proof

technique · direct
1.1F2F5givenalgebra

Fix p∈M and extend a g-orthonormal basis (e1,…,em) of TpM to local fields on M, lifted independently of t to the product. Write Ei(t)=dFt(ei) and Gij(t)=g‾(Ei(t),Ej(t)). In ambient coordinates, equality of mixed partials and the symmetric Christoffel symbols in [F5] give DtEi∣t=0=Dei(dF(∂t))∣t=0=∇‾eiV.

2.1F3F4F5step 1.1algebra

Metric compatibility and step 1.1 give G˙ij(0)=g‾(∇‾eiV,ej)+g‾(ei,∇‾ejV). At p, G(0)=I. Applying [F3]–[F4] therefore yields the pointwise density derivative ddt∣0μgt=12tr⁡(G˙(0))μg=∑i=1mg‾(∇‾eiV,ei)μg.

3.1F1F6step 2.1algebra

Because V is normal, [F6] converts each summand in step 2.1 to −g‾(V,IIf(ei,ei)). The trace formula [F1] now gives the global density identity ddt∣0μgt=−g‾ ⁣(V,∑iIIf(ei,ei))μg=−mg‾(V,Hf)μg. Both sides are intrinsic, so the pointwise calculation in an arbitrary orthonormal basis patches over M.

4.1F2F3F7F8step 3.1

Write μgt=J(t,p)μg on K. By [F2]–[F3], J is smooth and positive near {0}×K. Compactness supplies a closed parameter interval on which ∣∂tJ∣ is bounded; the constant bound is integrable because [F8] gives K finite volume. Thus [F7] passes the derivative through the fixed-domain integral, and step 3.1 gives AK′(0)=∫K∂tJ(0,p) μg=−m∫Kg‾(V,Hf) μg.

5.1F8step 4.1given

The last integrand in step 4.1 vanishes outside supp⁡V, which lies in int⁡MK. Its extension by zero is therefore a smooth compactly supported density on M, and locality of the intrinsic integral in [F8] gives ∫Kg‾(V,Hf)μg=∫Mg‾(V,Hf)μg. The same equality holds for every eligible K, proving domain independence.

6.1F1F9F10step 3.1step 4.1step 5.1algebra

Now assume M is boundaryless and drop the normality hypothesis. Decompose V=V⊤+V⊥. The tangent field corresponding to V⊤ is compactly supported inside int⁡MK, so [F9] supplies its flow ϕt, with ϕt equal to the identity near ∂K. Put F~t=Ft∘ϕt−1. Its variation field is V−df(V⊤)=V⊥, while ϕt(K)=K and [F10] gives Vol⁡F~t∗g‾(K)=Vol⁡Ft∗g‾(K). Applying steps 3.1–5.1 to F~ proves the same formula for the original variation, since g‾(V⊥,Hf)=g‾(V,Hf).

6.2step 5.1given

If M is compact, it is itself an eligible compact domain (its interior relative to itself is M), so step 5.1 gives the total-volume formula.

7.1F1F2F6F8F9F10step 1.1step 3.1step 4.1step 5.1step 6.1step 6.2∎

For empty M (of fixed positive dimension), both integrals and the derivative are zero. Dimension zero is excluded because the averaged vector contains 1/m; in dimension one the proof is the single diagonal Gram calculation. A zero variation field gives zero pointwise. Immersivity in [F2] excludes a degenerate pullback metric. The parameter value 0 is interior to (−ε,ε), and the density argument applies to the boundary of K without orientation or integration by parts. The all-variation clause is restricted to boundaryless M because [F9]'s two-sided reparametrizing flow need not exist for a field transverse to a manifold boundary. The stated ACω is inherited through [F1], [F6], and [F8]; [F9]–[F10], the pointwise finite-basis calculation, and one compactness bound add no choice.

Depends on

Used by

Dependency tree · two levels

74 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