Alphabeta Math
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.

Green's first identity on a glued elementary solid region

Statement

Let a finite gluing of elementary solid regions be given, with union E and outer boundary presentation Σout, let O be an open set containing E, let u:OR be C1 and let v:OR be C2. Then

E(u,v+uΔv)=Euv,n,

the right-hand side being the flux of the field uv over Σout.

No symmetry between u and v is claimed: the hypotheses on them differ.

Facts & Assumptions

Given: The finite gluing with union E and outer presentation Σout, the open OE, the C1 function u and the C2 function v on O.

[F1]

For scalar-valued f the gradient is f=(0f,,m1f) (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).

[F2]

For a C2 function f on an open subset of Rn, Δf=divf=i<niif (The Laplacian of a C2 function and of a C2 vector field).

[F3]

A scalar f is of class Ck on U when every iterated derivative of length at most k exists and is continuous on U (Ck maps and multi-index derivative notation in Euclidean space), and a map is Ck when each component is (Ck Euclidean maps and diffeomorphisms).

[F4]

For x,yRm, x,y=i<mxiyi (The Euclidean inner product x,y=k<nxkyk on Rn), and the divergence of a C1 field is divG=i<niGi (Divergence and curl of a C1 vector field).

[L1]

Let URn be open, let G:URn be C1 and let f:UR be C1. Then fG is C1 on U and div(fG)=f,G+fdivG (Divergence and curl are linear and satisfy the scalar product rules).

[L2]

For a finite gluing with union E and outer presentation Σout and a C1 field G on an open set containing E, EdivG=EG,n (The divergence theorem for finite gluings of elementary solid regions).

Proof

technique · direct
1.1

Since v is C2 on O, [F1] and [F3] make each component iv of v a function with continuous first partial derivatives, so v is a C1 field on O.

givenF1F3
2.1

The function u is C1 on O and v is a C1 field there by step 1.1, so [L1] with f=u and G=v makes uv a C1 field on O with div(uv)=u,v+udivv=u,v+uΔv, the last equality by [F2] and [F4].

step 1.1F2F4L1
3.1

Applying [L2] to the C1 field uv on the open OE and substituting step 2.1 on the left gives E(u,v+uΔv)=Euv,n, and by [F4] the boundary integrand is uv,n. That is the asserted identity.

step 2.1F4L2

Remarks

  • The regularity is asymmetric because the identity is. The left-hand side applies Δ to v and only to u, so v must be C2 and u need only be C1. Interchanging them is a different statement and needs u to be C2 as well; that is Green's second identity on a glued elementary solid region.

  • The boundary integrand is the normal derivative of v, weighted by u. The quantity v,n is the derivative of v in the direction of the boundary normal, and the identity says that its u-weighted boundary integral is controlled by Δv and by the pairing of the two gradients inside the solid. Taking u identically 1 makes the first volume term vanish, which is the form used on the companion examples page.

Depends on

Used by

Dependency tree · two levels

33 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