Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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.

Riemannian divergence theorem

Statement

Assume countable choice. On an oriented Riemannian manifold with boundary, n≥1, a smooth compactly supported vector field satisfies ∫M(div⁡gX)vol⁡g=∫∂Mg(X,ν)vol⁡∂g, with outward unit normal ν and outward-normal-first boundary orientation.

Facts & Assumptions

Given: The stated oriented manifold, vector field, and countable choice.

[F1]

Coordinate formula for riemannian divergence: In coordinates, div⁡gX=(det⁡G)−1/2∑i=1n∂i((det⁡G)1/2Xi).

[F2]

The riemannian volume form is the unique positive unit top form: The Riemannian volume form is the unique positive unit section of ⋀nT∗M for the specified orientation and normalized exterior metric.

[F3]

Pullback of a riemannian metric is riemannian exactly for immersions: F∗h is Riemannian if and only if F is an immersion. In general it is positive semidefinite, with radical ker⁡dFp at p.

[F4]

The general Stokes theorem: Assume ACω. Let M be an oriented smooth n-manifold with boundary, n≥1, and let η∈Ωcn−1(M). With j:∂M↪M and the outward-normal-first orientation, ∫Mdη=∫∂Mj∗η. An empty boundary contributes zero; in dimension one its integral is a finite signed sum of point values.

[F6]

Induced boundary orientation: For an oriented manifold with boundary, orient Tp∂M by the outward-normal-first rule: an outward vector first, followed by a positive boundary determinant, is a positive determinant of TpM.

[F7]

The boundary tangent space is the boundary-tangent hyperplane: For p∈∂M of an n≥1 dimensional manifold and the inclusion i:∂M↪M, the differential dip identifies Tp∂M with the hyperplane of boundary-tangent vectors in TpM.

[F8]

The gradient is characterized by inner products: The gradient is the unique smooth vector field Y satisfying g(Y,X)=Xf for every smooth vector field X.

[F9]

Riemannian metrics induce metrics on dual tensor and exterior bundles: A Riemannian metric induces smooth metrics on dual, tensor and exterior bundles. On decomposable covectors, ⟨α1∧⋯∧αk,β1∧⋯∧βk⟩=det⁡(⟨αi,βj⟩); increasing orthonormal wedge monomials have norm one.

[F10]

The Axiom of Countable Choice (ACω): The Axiom of Countable Choice, written ACω, is the following statement. > For every family (Xn)n∈N of nonempty sets indexed by > N there is a function f with domain N such that > f(n)∈Xn for every n∈N. Equivalently, in the vocabulary of def-choice-function: every at most countable family of nonempty sets (def-countable) has a choice function.

Proof

technique · direct
1.1F3F7F8given

In a boundary chart let u≥0 be its inward boundary coordinate. The boundary tangent space is ker⁡du. The gradient identity gives g(grad⁡u,v)=du(v), so the nonzero gradient is perpendicular to that hyperplane. Therefore ν=−grad⁡u/∣grad⁡u∣ is smooth, unit and outward, since du(ν)=−∣grad⁡u∣<0. The orthogonal complement is a line and exactly one of its two unit vectors is outward; hence these local definitions agree. The boundary inclusion is an immersion, so the induced metric is Riemannian.

2.1F2F6F9step 1.1

Write X=g(X,ν)ν+XT, with XT tangent to the boundary. The term vol⁡g(XT,v1,…,vn−1) vanishes because these n vectors lie in a hyperplane. On a positive orthonormal boundary basis the form j∗(ινvol⁡g) is positive and unit by the outward-first convention and the normalized exterior pairing. Uniqueness of the boundary volume form gives j∗(ιXvol⁡g)=g(X,ν)vol⁡∂g. For n=1, this identity uses the induced signed zero-form: its value is vol⁡g(ν)=ε∂, so the same scalar identity holds.

3.1F1F4F10step 2.1∎

The form η=ιXvol⁡g is smooth and supported in the compact support of X. In coordinates dη=∑i∂i(det⁡GXi) dx1∧⋯∧dxn=(div⁡gX)vol⁡g. Stokes under countable choice therefore gives ∫M(div⁡gX)vol⁡g=∫∂Mj∗η. Substitute step 2.1 to obtain the claimed formula. Empty boundary contributes zero, a zero field gives zero on both sides, and compact M permits every smooth field. In dimension one the oriented boundary integral is the finite signed endpoint sum.

Source locator

Lee, Propositions 15.32–15.33, pp.390–391, Lemma 16.30 and Theorem 16.32, pp.423–424; boundary and choice hypotheses are checked explicitly.

Depends on

Used by

Dependency tree · two levels

37 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