LemmaStatement: AI-adaptedProof: AI-generatedverified 2026-10-22 (gpt-6.1-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.

Stokes identity for a C1 two-form on the standard three-simplex

Physical scope

Pure mathematics; no physical premises or physical claim.

Statement

Let $T = {(u_{1}, u_{2}, u_{3}) \in R^{3} : u_{i} \geq 0, u_{1} + u_{2} + u_{3} \leq 1}$ with its positive affine orientation and signed outward boundary. Let $η = f_{1} d u^{2} \land d u^{3} - f_{2} d u^{1} \land d u^{3} + f_{3} d u^{1} \land d u^{2}$ be a $C^{1}$ two-form on an open neighbourhood of $T$ , and define

$d η = (\partial_{1} f_{1} + \partial_{2} f_{2} + \partial_{3} f_{3}) d u^{1} \land d u^{2} \land d u^{3} .$

Using the continuous-form chain integral of Continuous differential-form integrals over smooth singular chains in Euclidean domains,

$\int_{T} d η = \int_{\partial T} η .$

Statement references

Continuous differential-form integrals over smooth singular chains in Euclidean domains

Standard orientation of the affine simplex

Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$

Continuously differentiable maps, local inverses, and local diffeomorphisms

Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative

Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable

Change of variables for an injective $C^{1}$ map on a compact Jordan set

Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$

Facts & Assumptions

Given: The oriented simplex $T$ and the $C^{1}$ coefficient functions $f_{1}, f_{2}, f_{3}$ in the Statement.

[F1]

Continuous differential-form integrals over smooth singular chains in Euclidean domains defines both integrals by affine pullback coefficients, with the same positive parameter coordinates used in the Statement.

[F2]

Standard orientation of the affine simplex gives the signed-face formula $\partial [v_{0}, v_{1}, v_{2}, v_{3}] = [v_{1}, v_{2}, v_{3}] - [v_{0}, v_{2}, v_{3}] + [v_{0}, v_{1}, v_{3}] - [v_{0}, v_{1}, v_{2}]$ and the outward induced orientations.

[F3]

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 for a continuous derivative on a compact interval $[a, b]$ with $a < b$ .

[F4]

Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable integrates the continuous derivative coefficients over the coordinate sections of the compact Jordan simplex.

[F5]

Change of variables for an injective $C^{1}$ map on a compact Jordan set permits the affine coordinate changes between the upper face and its ordered simplex parameters, with the absolute determinant factor.

[F6]

Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ gives finite linearity and additivity of the Riemann integrals.

[F7]

Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ defines the coordinate derivatives used in the formula for $d η$ .

[F8]

Continuously differentiable maps, local inverses, and local diffeomorphisms defines continuously differentiable coefficient functions with continuous first derivative.

[F9]

The proof of Continuous differential-form integrals over smooth singular chains in Euclidean domains establishes that every standard affine simplex is compact Jordan and every continuous pullback coefficient on it is Riemann integrable. In particular, this applies to $T$ and each $D_{i}$ .

Proof

Given: The oriented simplex $T$ and $C^{1}$ form $η$ in the Statement.

1.1F3F4F7F8F9given

Each $D_{i} = {u_{j} \geq 0 : j \neq i, \sum_{j \neq i} u_{j} \leq 1}$ is the standard two-simplex up to a coordinate permutation, and $T$ is the standard three-simplex, so [F9] gives that all are compact Jordan. The coefficient functions $f_{i}$ and $\partial_{i} f_{i}$ are continuous on them by the $C^{1}$ hypothesis [F8], so their integrals exist by [F9]. Fix $i$ and fix the other two coordinates in $D_{i}$ . The $u_{i}$ -section of $T$ is $[0, 1 - \sum_{j \neq i} u_{j}]$ . If $1 - \sum_{j \neq i} u_{j} > 0$ , [F3] makes its integral of $\partial_{i} f_{i}$ the upper endpoint value of $f_{i}$ minus the lower endpoint value. If the upper endpoint is $0$ , the section is a singleton: its bounded integrand has zero integral (cover the point by intervals of arbitrarily small length), and the endpoint difference is also zero. Thus the same identity holds for every section. Integrating this identity over $D_{i}$ by [F4], then summing over $i$ , writes $\int_{T} d η$ as the sum of all upper endpoint terms minus all lower endpoint terms.

2.1F2step 1.1

On the three lower faces, in increasing order of their remaining coordinates, the induced boundary integrals are $- \int f_{1} d u^{2} \land d u^{3}$ on $u_{1} = 0$ , $- \int f_{2} d u^{1} \land d u^{3}$ on $u_{2} = 0$ , and $- \int f_{3} d u^{1} \land d u^{2}$ on $u_{3} = 0$ . The first and third signs are the boundary signs in [F2]; the middle face has positive signed face but the restriction of $η$ is already $- f_{2} d u^{1} \land d u^{3}$ . Thus the lower endpoint terms from step 1.1 are exactly the three lower-face contributions to $\int_{\partial T} η$ .

3.1F1F2F5F6step 1.1step 2.1given∎

On the upper face, set $u_{1} = 1 - u_{2} - u_{3}$ . Substitution gives $η ∣_{u_{1} + u_{2} + u_{3} = 1} = (f_{1} + f_{2} + f_{3}) d u^{2} \land d u^{3}$ . Its outward normal is proportional to $(1, 1, 1)$ , while the ordered tangent vectors $(- 1, 1, 0), (- 1, 0, 1)$ have cross product $(1, 1, 1)$ , so $(u_{2}, u_{3})$ gives the positive face orientation. The ordered affine face parameters differ from $(u_{2}, u_{3})$ by an affine map with determinant of absolute value $1$ ; [F5] therefore identifies the upper endpoint sum in step 1.1 with the upper-face integral. Adding the four face contributions using [F6] proves $\int_{T} d η = \int_{\partial T} η$ .

Stokes identity for a C1 two-form on the standard three-simplex

Statement

Statement references

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources