CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

Vector forms: the boundary integrals of $f n$ and of $n \times F$

Statement

Let a finite gluing of elementary solid regions be given, with union $E$ and outer boundary presentation $Σ^{o u t} = ((D_{1}, φ_{1}), \dots, (D_{M}, φ_{M}))$ . Vector-valued integrals below are taken coordinatewise, so that for a continuous $R^{3}$ -valued $W$ on $E$ the symbol $∭_{E} W$ denotes the vector whose $k$ th coordinate is $\int_{E} W_{k}$ , and for a continuous $R^{3}$ -valued $Z$ on the boundary the symbol $\iint_{\partial E} Z$ denotes the vector whose $k$ th coordinate is $\sum_{j = 1}^{M} \int_{D_{j}} Z_{k} (φ_{j})$ , where $n$ inside such an integrand is read as the oriented area vector $φ_{j, u} \times φ_{j, v}$ of the patch, exactly as in the scalar flux.

Then, for $f$ of class $C^{1}$ on an open set containing $E$ and $F$ of class $C^{1}$ on an open set containing $E$ ,

$∭_{E} \nabla f = \iint_{\partial E} f n, ∭_{E} curl F = \iint_{\partial E} n \times F .$

Facts & Assumptions

Given: The finite gluing with union $E$ and outer presentation $Σ^{o u t}$ , the $C^{1}$ scalar $f$ and the $C^{1}$ field $F$ , both on open sets containing $E$ , and the coordinatewise reading of the vector integrals fixed in the Statement.

[F1]

The divergence of a $C^{1}$ field is $div G = \sum_{i < n} \partial_{i} G_{i}$ and the curl of a $C^{1}$ field on an open subset of $R^{3}$ is $curl G = (\partial_{y} G_{z} - \partial_{z} G_{y}, \partial_{z} G_{x} - \partial_{x} G_{z}, \partial_{x} G_{y} - \partial_{y} G_{x})$ (Divergence and curl of a $C^{1}$ vector field).

[F2]

For $u = (u_{x}, u_{y}, u_{z})$ and $v = (v_{x}, v_{y}, v_{z})$ in $R^{3}$ , $u \times v = (u_{y} v_{z} - u_{z} v_{y}, u_{z} v_{x} - u_{x} v_{z}, u_{x} v_{y} - u_{y} v_{x})$ (The cross product in $R^{3}$ ).

[F3]

For $x, y \in R^{m}$ , $⟨ x, y ⟩ = \sum_{i < m} x_{i} y_{i}$ , and $e_{k}$ has $k$ th coordinate $1$ and the others $0$ , so $⟨ x, e_{k} ⟩ = x_{k}$ (The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ , The standard list $e : n \to F^{n}$ with $e_{i} (i) = 1_{F}$ and $e_{i} (j) = 0_{F}$ for $j \neq i$ is an ordered basis of $F^{n}$ ; hence $\dim_{F} F^{n} = n$ , and $F^{0}$ is the zero space with basis $\emptyset$ and dimension $0$ ).

[F4]

For scalar-valued $f$ the gradient is $\nabla f = (\partial_{0} f, \dots, \partial_{m - 1} f)$ (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[F5]

In a finite gluing the outer patches form a compatible finite patch presentation of $\partial E$ , over which flux is the sum of the patch values (Finite gluings of elementary solid regions and their outward boundary presentation, Finitely patched regular surfaces, their area, scalar integrals, and flux).

[L1]

For $C^{1}$ fields and a $C^{1}$ scalar on an open subset of $R^{n}$ , $div (g G) = ⟨ \nabla g, G ⟩ + g div G$ (Divergence and curl are linear and satisfy the scalar product rules).

[L2]

For $C^{1}$ fields $G, H$ on an open subset of $R^{3}$ , $div (G \times H) = ⟨ curl G, H ⟩ - ⟨ G, curl H ⟩$ (The divergence and curl of a cross product).

[L3]

For a finite gluing with union $E$ and outer presentation $Σ^{o u t}$ and a $C^{1}$ field $G$ on an open set containing $E$ , $∭_{E} div G = \iint_{\partial E} ⟨ G, n ⟩$ (The divergence theorem for finite gluings of elementary solid regions).

Proof

technique · direct

1.1

Let $c \in R^{3}$ and let $\underline{c}$ be the constant field with value $c$ on the open set where $f$ is $C^{1}$ . Its partial derivatives all vanish, so it is $C^{1}$ with $div \underline{c} = 0$ and $curl \underline{c} = 0$ by [F1]. The field $f \underline{c}$ is $C^{1}$ and [L1] gives $div (f \underline{c}) = ⟨ \nabla f, \underline{c} ⟩ + f div \underline{c} = ⟨ \nabla f, c ⟩$ , while its flux integrand against a vector $ν$ is $⟨ f c, ν ⟩ = f ⟨ c, ν ⟩$ by [F3].

givenF1F3L1

1.2

For all $a, b, d \in R^{3}$ , expanding both sides by [F2] and [F3] gives $⟨ a \times b, d ⟩ = (a_{y} b_{z} - a_{z} b_{y}) d_{x} + (a_{z} b_{x} - a_{x} b_{z}) d_{y} + (a_{x} b_{y} - a_{y} b_{x}) d_{z},$ $⟨ d \times a, b ⟩ = (d_{y} a_{z} - d_{z} a_{y}) b_{x} + (d_{z} a_{x} - d_{x} a_{z}) b_{y} + (d_{x} a_{y} - d_{y} a_{x}) b_{z},$ and the six monomials of the first list are the six of the second with the same signs, matched as $a_{y} b_{z} d_{x}$ with $d_{x} a_{y} b_{z}$ , $- a_{z} b_{y} d_{x}$ with $- d_{x} a_{z} b_{y}$ , $a_{z} b_{x} d_{y}$ with $d_{y} a_{z} b_{x}$ , $- a_{x} b_{z} d_{y}$ with $- d_{y} a_{x} b_{z}$ , $a_{x} b_{y} d_{z}$ with $d_{z} a_{x} b_{y}$ and $- a_{y} b_{x} d_{z}$ with $- d_{z} a_{y} b_{x}$ . Hence $⟨ a \times b, d ⟩ = ⟨ d \times a, b ⟩$ .

F2F3algebra

2.1

With $\underline{c}$ as in step 1.1 on the open set where $F$ is $C^{1}$ , the field $F \times \underline{c}$ is $C^{1}$ and [L2] gives $div (F \times \underline{c}) = ⟨ curl F, c ⟩ - ⟨ F, curl \underline{c} ⟩ = ⟨ curl F, c ⟩$ .

givenF1F2L2

2.2

Apply [L3] to the field $f \underline{c}$ of step 1.1: $\int_{E} ⟨ \nabla f, c ⟩ = \sum_{j = 1}^{M} \int_{D_{j}} f (φ_{j}) ⟨ c, φ_{j, u} \times φ_{j, v} ⟩$ , using [F5] to read the right side patch by patch. Take $c = e_{k}$ : by [F3] and [F4] the left side becomes $\int_{E} \partial_{k} f$ , the $k$ th coordinate of $∭_{E} \nabla f$ , and the right side becomes $\sum_{j} \int_{D_{j}} f (φ_{j}) (φ_{j, u} \times φ_{j, v})_{k}$ , the $k$ th coordinate of $\iint_{\partial E} f n$ . As $k$ ranges over the three directions this is the first identity.

step 1.1F3F4F5L3

3.1

Apply [L3] to the field $F \times \underline{c}$ of step 2.1: $\int_{E} ⟨ curl F, c ⟩ = \sum_{j = 1}^{M} \int_{D_{j}} ⟨ F (φ_{j}) \times c, φ_{j, u} \times φ_{j, v} ⟩$ . Step 1.2 with $a = F (φ_{j})$ , $b = c$ and $d = φ_{j, u} \times φ_{j, v}$ rewrites each integrand as $⟨ (φ_{j, u} \times φ_{j, v}) \times F (φ_{j}), c ⟩$ . Take $c = e_{k}$ : by [F3] the left side becomes $\int_{E} (curl F)_{k}$ and the right side becomes $\sum_{j} \int_{D_{j}} ((φ_{j, u} \times φ_{j, v}) \times F (φ_{j}))_{k}$ , so as $k$ ranges over the three directions this is the second identity.

step 2.1step 1.2F3F5L3

4.1

Steps 2.2 and 3.1 are the two asserted identities.

step 2.2step 3.1∎

Remarks

Why a constant vector is the right device. Both clauses assert an equality of vectors, and the divergence theorem produces only scalars. Pairing with a fixed $c$ turns each vector identity into a scalar one; running $c$ over the standard basis recovers the vector identity coordinate by coordinate, and nothing else about $c$ is used.
The triple-product identity of step 1.2 is the determinant identity in disguise. By The cross product is bilinear, alternating, and orthogonal to both factors each of $⟨ a \times b, d ⟩$ and $⟨ d \times a, b ⟩$ is the determinant of the matrix with the three vectors as columns, in the orders $a, b, d$ and $d, a, b$ ; those two orders differ by a cyclic permutation of three columns. The coordinate expansion above is the same fact written out, and it is what the proof uses.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

50 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

J. Feldman, A. Rechnitzer and E. Yeager, CLP-4 Vector Calculus (University of British Columbia), Theorem 4.2.9 (standard reference, not scraped)

Vector forms: the boundary integrals of fnfn and of n×Fn×F