Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck 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 second 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, and let u,v:O→R both be C2. Then

∭E(uΔv−vΔu)=∬∂E(u⟨∇v,n⟩−v⟨∇u,n⟩).

Both functions are required to be C2, which is a stronger hypothesis than the first identity places on either of them.

Facts & Assumptions

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

[F1]

For scalar-valued f the gradient is ∇f=(∂0f,…,∂m−1f) (The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case), and Δf=div⁡∇f for C2 f (The Laplacian of a C2 function and of a C2 vector field).

[F2]

For x,y∈Rm, ⟨x,y⟩=∑i<mxiyi; in particular ⟨x,y⟩=⟨y,x⟩ (The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn).

[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; in particular a C2 function is C1 (Ck maps and multi-index derivative notation in Euclidean space).

[F4]

The flux over a finite patch presentation is a finite sum of parameter integrals of continuous integrands (The divergence theorem for finite gluings of elementary solid regions).

[L1]

Under the hypotheses above with u of class C1 and v of class C2, ∭E(⟨∇u,∇v⟩+uΔv)=∬∂Eu⟨∇v,n⟩ (Green's first identity on a glued elementary solid region).

[L2]

For integrable f,g on a nondegenerate rectangle and scalars α,β, the function αf+βg is integrable with integral α∫f+β∫g (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm).

[L3]

Every continuous real function on a compact Jordan measurable set is Riemann integrable over it (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set), and for a finite gluing E is compact and Jordan measurable (Internal faces cancel and volume integrals add when elementary solid regions are glued).

Proof

technique · direct
1.1givenF3L1

Both u and v are C2 on O, hence also C1 there by [F3]. So [L1] applies as it stands and gives ∭E(⟨∇u,∇v⟩+uΔv)=∬∂Eu⟨∇v,n⟩; and it applies again with the roles of the two functions exchanged, which is legitimate exactly because both are C2, giving ∭E(⟨∇v,∇u⟩+vΔu)=∬∂Ev⟨∇u,n⟩.

2.1givenF1F3F4L2L3

All the integrands appearing in step 1.1 are continuous: ∇u and ∇v have continuous components by [F1] and [F3], Δu and Δv are continuous by [F1] and [F3], and each boundary integrand is a continuous function on a compact Jordan parameter region by [F4]. So every one of them is integrable over the relevant set by [L3], and differences of them may be taken inside the integrals by [L2].

3.1step 1.1step 2.1F2L2∎

Subtract the second identity of step 1.1 from the first, using step 2.1 to combine the integrals. By the symmetry of the inner product in [F2] the two terms ⟨∇u,∇v⟩ and ⟨∇v,∇u⟩ are equal and cancel, leaving ∭E(uΔv−vΔu) on the left and ∬∂E(u⟨∇v,n⟩−v⟨∇u,n⟩) on the right.

Remarks

  • What the extra hypothesis buys. The first identity needs only one of the two functions to be C2; using it twice with the roles exchanged needs both. That is the whole difference between the two identities, and it is why the second is stated separately rather than as a rearrangement of the first.

  • The cancellation is the symmetry of the inner product, nothing more. No integration by parts and no mixed-partials theorem enters here: the term that cancels is literally the same function written two ways.

Depends on

Used by

Dependency tree · two levels

57 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