Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

A function with vanishing Laplacian has zero boundary flux of its gradient on the unit box

Example

Let v(x,y,z)=x2y2 on the closed unit box B=[0,1]3. Then Δv=0, so Green's first identity with u1 gives zero boundary flux for v. Directly, the six face contributions are 2,0,2,0,0,0, so they do sum to 0.

Facts & Assumptions

Given: The function v(x,y,z)=x2y2, the constant function u1, and the closed unit box with the six-patch presentation of The closed unit box, with its six faces, is an elementary solid region.

[L1]

For a finite gluing of elementary solid regions, with u of class C1 and v of class C2 on an open neighbourhood of the union, Green's first identity reads E(u,v+uΔv)=Euv,n (Green's first identity on a glued elementary solid region).

[F1]

The Laplacian is Δf=divf (The Laplacian of a C2 function and of a C2 vector field).

[L2]

The closed unit box has the six outward faces of The closed unit box, with its six faces, is an elementary solid region. [ex-the-closed-unit-box-is-an-elementary-solid-region]

[L3]

The divergence theorem is EdivF=EF,n (The divergence theorem on an elementary solid region).

[F2]
[F3]

The divergence is the sum of the coordinate partial derivatives (Divergence and curl of a C1 vector field).

[L4]

For a bounded Jordan set and an integrable function whose sections are integrable outside a content-zero exceptional set, Jordan Fubini computes the multiple integral by iterated section integrals (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable).

[L5]

If a<b, G is differentiable on [a,b], and G=f is integrable there, then abf=G(b)G(a) (The second fundamental theorem: if G is differentiable on [a,b] with G=f and f is integrable, then abf=G(b)G(a)).

[F4]

Verification

technique · direct
1.1

One has v=(2x,2y,0), hence Δv=x(2x)+y(2y)+z0=22+0=0 by [F1], [F2], [F3], and [L6].

F1F2F3L6given
2.1

Since u=0 and Δv=0, [L1] gives Bv,n=0 on the unit box of [L2], viewed as the one-piece gluing of that elementary solid region; this is the same conclusion [L3] would give for the field v.

step 1.1L1L2L3F4
2.2

On the face x=1 the outward unit normal is ex, so v,n=2 and the flux contribution is 2 by [L4] and [L5]; on the face x=0 it is 0.

step 1.1L2F2F4L4L5
2.3

On the face y=1 the outward unit normal is ey, so v,n=2 and the contribution is 2; on the face y=0 it is 0.

step 1.1L2F2F4L4L5
2.4

The third component of v is 0, so the two faces z=0 and z=1 contribute nothing.

step 1.1L2F2F4
3.1

The six face values add to 2+02+0+0+0=0, agreeing with step 2.1. This is a check of Green's identity on one harmonic polynomial, not a proof of the identity.

step 2.1step 2.2step 2.3step 2.4

Remarks

  • The example is deliberately asymmetric: the cancellation comes from the opposite signs of the x and y second derivatives, not from any symmetry between opposite faces.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

64 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