Alphabeta Math
LemmaStatement: AI-adaptedProof: 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.

The single-direction flux identity on a simple solid region

Statement

Let (k,D,γ1,γ2) be a simple description of a solid E in the direction k and let Σ=((D1,φ1),,(DP,φP)) be a boundary presentation adapted to it (Boundary presentations adapted to a simple solid region in a coordinate direction). Let R be a real function of class C1 on an open set containing E and let Rek be the field whose kth coordinate is R and whose other two coordinates are zero. Then the flux of Rek over the presentation equals the integral of the kth partial derivative of R over E:

j=1PDjRek(φj),φj,u×φj,v=EkR.

Facts & Assumptions

Given: The simple description (k,D,γ1,γ2) of E, the adapted presentation Σ with its supplied sublists Σ+,Σ,Σ0, and the function R of class C1 on an open OE. Write ψj=πkφj, Vj=ψj[Dj], σk1(w,t) for the point with πk-projection w and kth coordinate t, and Rγi(w):=R(σk1(w,γi(w))) for i=1,2.

[F1]

For a compatible finite patch presentation, the oriented flux is the sum of the patch values, each patch value being Dj(Fφj)(φj,u×φj,v) (Finitely patched regular surfaces, their area, scalar integrals, and flux, Unit normal fields, orientations, and flux through a regular surface patch).

[F2]

For jΣ0 the kth coordinate of φj,u×φj,v vanishes on the interior of Dj; the projected images of the upper sublist are pairwise disjoint and fill D up to content zero, and the same holds for the lower sublist (Boundary presentations adapted to a simple solid region in a coordinate direction).

[F3]

A regular patch has a compact Jordan parameter region that is the closure of its nonempty interior, and its parametrization is C1 on an open neighbourhood of that region (Regular parametrized surface patches on compact Jordan parameter regions).

[F4]

The simple solid region described by (k,D,γ1,γ2) is E={pR3:πk(p)D, γ1(πk(p))pkγ2(πk(p))} with D compact Jordan and γ1γ2 continuous on D, and σk(p)=(πk(p),pk) carries E onto the solid between the graphs of γ1 and γ2 over D (Simple solid regions in a coordinate direction and their cyclic coordinate projection).

[F5]

For x,yRm, x,y=i<mxiyi (The Euclidean inner product x,y=k<nxkyk on Rn); a C1 function has continuous first partial derivatives (Ck Euclidean maps and diffeomorphisms); and k is the kth partial derivative appearing in the divergence of Divergence and curl of a C1 vector field.

[F6]

Integration over a bounded Jordan measurable set is integration of the zero extension over a bounding rectangle (The Riemann integral of a bounded function over a bounded Jordan measurable set).

[L1]

For jΣ+ the flux of Rek through (Dj,φj) is VjRγ2, and for jΣ it is VjRγ1; each Vj is a bounded open Jordan measurable subset of D and the base integrand is integrable over it (The flux of a single-component field through a graph face is a base integral of its trace).

[L2]

Let A be bounded Jordan measurable, let N1 and let A1,,ANA be bounded Jordan sets with pairwise intersections of content zero and with AiAi of content zero; if f is bounded on A and integrable over A and over each Ai, then Af=i=1NAif (Additivity of the integral over finitely many Jordan pieces that fill a Jordan set up to content zero).

[L3]

For compact Jordan DRm, continuous αβ on D and K={(u,t):uD, α(u)tβ(u)}, the solid K is compact and Jordan measurable and every continuous H:KR satisfies KH=D(α(u)β(u)H(u,t)dt)du (A solid between continuous graphs over a compact Jordan base is Jordan measurable and integrates by vertical sections).

[L4]

For a cyclic coordinate permutation σk of R3 and compact Jordan E, the set σk[E] is compact Jordan and σk[E]H=EHσk for bounded H integrable on either side (A cyclic permutation of the coordinates of R3 preserves Jordan measurability and integrals).

[L5]

If G is differentiable at every point of [a,b] with a<b and G is integrable on [a,b], then abG=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)).

[L6]

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).

[L7]

For a C1 map φ of two variables into R3, (φu×φv)k=detD(πkφ) (Each coordinate of the oriented area vector is the Jacobian determinant of the matching cyclic projection).

Proof

technique · direct
1.1

Let jΣ0. By [F5] the flux integrand of Rek through (Dj,φj) is R(φj)(φj,u×φj,v)k, which is continuous on Dj because φj is C1 there by [F3] and R is continuous. By [F2] its second factor vanishes on Dj, and Dj is the closure of Dj by [F3], so a continuous function vanishing on Dj vanishes on Dj. Hence that patch's flux is Dj0=0.

givenF2F3F5L7
1.2

By [F4] the set E is compact and Jordan measurable and σk[E]=K:={(w,t):wD, γ1(w)tγ2(w)}. The function H(w,t):=(kR)(σk1(w,t)) is continuous on K, since kR is continuous on O by [F5] and σk1 is linear, and Hσk=kR on E. So [L4] applied with E=E gives EkR=KH, both integrals existing by [L3] and [L6].

givenF4F5L3L4L6
1.3

Fix wD and put G(t):=R(σk1(w,t)), defined and differentiable for every t with σk1(w,t)O, with G(t)=(kR)(σk1(w,t))=H(w,t) because varying t moves only the kth coordinate. If γ1(w)<γ2(w) then G is differentiable on [γ1(w),γ2(w)], whose points lie in EO by [F4], and G is continuous there hence integrable, so [L5] gives γ1(w)γ2(w)H(w,t)dt=G(γ2(w))G(γ1(w))=Rγ2(w)Rγ1(w). If instead γ1(w)=γ2(w) then the interval is degenerate, so the integral is 0, and the increment Rγ2(w)Rγ1(w) is also 0; the identity holds in that case too.

givenF4F5L5
1.4

The functions Rγ1 and Rγ2 are continuous on the compact Jordan base D, hence bounded and integrable over D by [L6] and [F6]. By [L1] each Vj with jΣ+ is a bounded Jordan subset of D over which Rγ2 is integrable, and by [F2] those sets are pairwise disjoint — so their pairwise intersections are empty and have content zero — and their union omits from D only a set of content zero. So [L2] gives jΣ+VjRγ2=DRγ2, and by [L1] the left side is the sum of the upper faces' fluxes.

givenF2F6L1L2L6
1.5

The same argument applied to the lower sublist gives jΣVjRγ1=DRγ1, and by [L1] each lower face's flux is VjRγ1, so the lower faces' fluxes sum to DRγ1.

givenF2F6L1L2L6
2.1

By step 1.3 the inner integral in [L3] is Rγ2(w)Rγ1(w) for every wD, a continuous function of w; so [L3] applied to H on K and step 1.2 give EkR=KH=D(Rγ2Rγ1)=DRγ2DRγ1, the last step by linearity of the integral over D.

step 1.2step 1.3L3L6
2.2

By [F1] the flux over the presentation is the sum of the P patch fluxes, which splits along the three supplied sublists. Step 1.1 makes the lateral sum zero, step 1.4 makes the upper sum DRγ2 and step 1.5 makes the lower sum DRγ1, so the total is DRγ2DRγ1.

step 1.1step 1.4step 1.5F1
3.1

Steps 2.1 and 2.2 give the same number for the two sides of the asserted identity, so it holds.

step 2.1step 2.2

Remarks

Depends on

Used by

Dependency tree · two levels

77 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