LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedverified 2026-09-23 (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.

Compact-support Stokes on the upper half-space

Statement

Give $H^{n} = {x_{n} \geq 0}$ the standard orientation, $n \geq 1$ , and its face the outward-normal-first orientation. If $η \in Ω_{c}^{n - 1} (H^{n})$ and $j : \partial H^{n} ↪ H^{n}$ , then $\int_{H^{n}} d η = \int_{\partial H^{n}} j^{*} η .$ These are the signed single-chart integrals of Chart integral with its orientation sign: the identity chart on $H^{n}$ and the standard chart on its face. Their compact supports lie in these global charts, so the identity requires no global partition of unity or choice axiom. Where the general manifold integral is available, its value agrees with this single-chart convention. With $η = \sum_{i} a_{i} d x^{1} \land \dots \land \hat{d x^{i}} \land \dots \land d x^{n}$ , both sides are $(- 1)^{n} \int_{R^{n - 1}} a_{n} (x^{'}, 0) d x^{'}$ for $n > 1$ , and $- a_{1} (0)$ for $n = 1$ .

Facts & Assumptions

[F1]

Chart integral with its orientation sign defines the signed integral of a compactly supported top form inside one connected chart, including a half-space chart and a signed point when the dimension is zero. Its coefficient zero extension across a face is Riemann integrable.

[F2]

Induced boundary orientation orients the face by the outward-normal-first rule.

[F3]

Form calculus extends locally across a manifold boundary gives the coordinate exterior derivative and support containment $supp (d η) \subseteq supp (η)$ , including at the face.

[F4]

A continuous function on a closed rectangle has repeated Riemann integrals in every coordinate order, all equal to its multiple integral permits iterated integration of continuous coefficients on a compact rectangle in either coordinate order. Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative gives the endpoint difference of each one-variable derivative integral.

Proof

Given: The objects and hypotheses in the statement above.

1.1F1F3F4

Compact support gives $R > 0$ such that $supp η$ is contained in $(- R, R)^{n - 1} \times [0, R)$ and misses all artificial outer faces. By [F3], $d η = \sum_{i = 1}^{n} (- 1)^{i - 1} \partial_{i} a_{i} d x^{1} \land \dots \land d x^{n},$ and its support lies in the same rectangle. The identity-chart integral [F1] is the Riemann integral of this coefficient on $[- R, R]^{n - 1} \times [0, R]$ ; zero extension across $x_{n} = 0$ does not change its value. For $n > 1$ , [F4] puts each $x_{i}$ integral first. The one-variable fundamental theorem gives zero for $i < n$ , since both artificial endpoint values vanish, and gives $- a_{n} (x^{'}, 0)$ for $i = n$ . Multiplying by $(- 1)^{n - 1}$ yields $(- 1)^{n} \int_{R^{n - 1}} a_{n} (x^{'}, 0) d x^{'}$ . For $n = 1$ , the same fundamental theorem directly gives $- a_{1} (0)$ .

2.1F1F2step 1.1

The face is closed, so the restriction of the compact support is compact there. Pullback to the face kills every term containing $d x^{n}$ , leaving $a_{n} (x^{'}, 0) d x^{1} \land \dots \land d x^{n - 1}$ . The outward vector is $- e_{n}$ , and $(- e_{n}, e_{1}, \dots, e_{n - 1})$ has determinant $(- 1)^{n}$ in the ambient standard frame. Thus [F1, F2] make the face-chart integral $(- 1)^{n} \int_{R^{n - 1}} a_{n} (x^{'}, 0) d x^{'}$ , exactly the value in step 1.1.

3.1F1F2step 1.1step 2.1∎

For $n = 1$ , the outward vector at zero is $- e_{1}$ , so [F1, F2] give the determinant-line point sign $- 1$ and boundary integral $- a_{1} (0)$ . This is the same endpoint difference from step 1.1. If the form is zero or its support misses the face, the same formulas give zero on both sides.

Depends on

Used by

The wrong boundary sign in the half-space computation Counterexample
Stokes on an interval with both endpoint chart signs Example
The general Stokes theorem Theorem

Dependency tree · two levels

25 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

Lee Theorem 16.11 proof, pp.412–413 (standard reference, not scraped)