Alphabeta Math
Session-authored (Fable 5 assisted)
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.

14 results · all verified · 10 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 4 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Regular Surfaces and Surface Integrals

1 · Prerequisites

2 · Summary

line-integrals-and-the-gradient-theorem supplies parametrized integration, orientation-sensitive line integrals, and the compact-Jordan change-of-variables setting inherited through its declared prerequisites. constant-rank-submersions-and-regular-level-sets supplies local graph coordinates and kernel tangent spaces for regular scalar levels. Euclidean inner products and Gram determinants provide the linear-algebraic area scale, while compactness supplies finite subcovers of local patches.

The cross product, regular surface patches, tangent planes, reparametrizations, the first fundamental form, area density, scalar surface integrals, orientations, and flux are developed first. The signed area-vector transformation yields the scalar and flux reparametrization laws, and content-zero seams support compatible finite patch presentations. Regular level surfaces are reconciled with patch tangent planes. Graph and surface-of-revolution formulas then reduce geometric areas and fluxes to compact Jordan integrals.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The cross product in R3

Definition

For u=(ux,uy,uz) and v=(vx,vy,vz) in R3, define u×v=(uyvzuzvy,uzvxuxvz,uxvyuyvx).

This is the right-handed cross product. The displayed coordinates are those of the standard basis (The standard list e:nFn with ei(i)=1F and ei(j)=0F for ji is an ordered basis of Fn; hence dimFFn=n, and F0 is the zero space with basis and dimension 0), and inner products and norms are those of The Euclidean inner product x,y=k<nxkyk on Rn.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The cross product is bilinear, alternating, and orthogonal to both factors

Statement

For all u,v,wR3, the cross product is bilinear and alternating, u×v,w=det[u v w], and u×v is orthogonal to both u and v.

Facts & Assumptions

Given: Vectors u,v,wR3 and a scalar cR.

[L1]

The cross product is given by its three coordinate differences of products (The cross product in R3), and the Euclidean inner product is the coordinate dot product (The Euclidean inner product x,y=k<nxkyk on Rn).

Proof

technique · direct
1.1

Substitution in [L1] gives (u+u)×v=u×v+u×v, (cu)×v=c(u×v), and the corresponding two identities in the second argument.

L1algebra
1.2

The same coordinate formula gives u×u=0 and v×u=(u×v), so the product is alternating.

L1algebra
1.3

Expanding the dot product in [L1] yields u×v,w=(uyvzuzvy)wx+(uzvxuxvz)wy+(uxvyuyvx)wz, which is the determinant det[u v w] by [L2].

L1L2algebra
2.1

Taking w=u or w=v makes the determinant have two equal columns and hence zero; therefore u×v is orthogonal to both factors. The calculation includes zero and parallel vectors.

step 1.3L2algebra
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The squared cross-product norm is the Gram determinant of two vectors

Statement

For u,vR3, u×v22=detG(u,v), and this value is positive exactly when u and v are linearly independent.

Equivalently, u×v22=u22v22u,v2.

Facts & Assumptions

Given: Vectors u,vR3.

[L1]

The cross product has the displayed coordinate formula, and it is bilinear, alternating, and orthogonal to its factors (The cross product in R3, The cross product is bilinear, alternating, and orthogonal to both factors).

[L2]

The two-vector Gram matrix has entries ui,uj, and its determinant is positive exactly for a linearly independent pair and zero exactly for a dependent pair (The Gram matrix G(v0,,vr1)=(vi,vj)i,j<r and Gram determinant, with empty value 1, A Gram determinant is nonnegative and is positive exactly when the vector list is linearly independent).

Proof

technique · direct
1.1

Expanding the three squared coordinates of u×v and collecting terms gives u×v22=(ux2+uy2+uz2)(vx2+vy2+vz2)(uxvx+uyvy+uzvz)2.

givenL1algebra
2.1

The right side of step 1.1 is u22v22u,v2=det(u,uu,vv,uv,v), which is detG(u,v) by [L2].

step 1.1L2algebra
3.1

The positivity and vanishing assertions follow from [L2], including the cases in which either vector is zero.

step 2.1L2
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Regular parametrized surface patches on compact Jordan parameter regions

Definition

A compact Jordan parameter region is a compact Jordan measurable set DR2 that is the closure of its nonempty connected interior D (The Riemann integral of a bounded function over a bounded Jordan measurable set, Interior, closure, boundary, limit point, isolated point and dense subset of a metric space). Its boundary has content zero (A bounded set in Rm is Jordan measurable iff its boundary is null, equivalently of content zero).

A regular parametrized surface patch is the image of a C1 map from a compact Jordan parameter region whose parameter cross product is nonzero on the region's interior and for which no interior parameter point shares its image with a distinct point of the whole region. Seam identifications and rank failures may occur only on the boundary. Here C1 is the Euclidean componentwise class of Ck Euclidean maps and diffeomorphisms. More precisely, the parametrization φ is defined on an open neighbourhood of D, φu×φv0 on D, and no point of D has the same image as a distinct point of D. The chosen pair (D,φ) is part of the patch data.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The tangent plane of a regular surface patch

Definition

Let (D,φ) be a regular parametrized surface patch (Regular parametrized surface patches on compact Jordan parameter regions) and let p=φ(u,v) with (u,v)D. At an interior parameter point, the tangent plane is span{φu,φv}.

The two spanning vectors are linearly independent because their cross product is nonzero (The squared cross-product norm is the Gram determinant of two vectors), so this is a two-dimensional linear subspace of R3 (Linear combination of a finite list, and the span span(S) as the smallest linear subspace containing S). The affine tangent plane through p is p+span{φu,φv}.

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-24Open item page →

Surface reparametrizations and their orientation sign

Definition

Let (D,φ) and (E,ψ) be regular surface patches. A regular reparametrization from ψ to φ is a C1 diffeomorphism h between neighbourhoods of their compact Jordan parameter regions with ψ=φh. We additionally require h[E]=D (Ck Euclidean maps and diffeomorphisms).

The derivative Dh is invertible, so its Jacobian determinant is nonzero (The Jacobian determinant of a square-dimensional C1 map is the determinant of its Jacobian matrix). A regular surface reparametrization is orientation-preserving when its parameter Jacobian determinant is positive and orientation-reversing when it is negative. Constancy of the sign on a connected parameter region is proved separately; the terms here apply pointwise whenever needed.

PropositionStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The tangent plane is invariant under regular reparametrization

Statement

Regular reparametrizations preserve the tangent plane at corresponding interior parameter points.

Precisely, if ψ=φh and (s,t) is interior, then span{ψs,ψt}=span{φu,φv}h(s,t).

Facts & Assumptions

Given: A regular reparametrization ψ=φh and an interior parameter point (s,t).

[L1]

The tangent plane is the span of the two parameter derivatives (The tangent plane of a regular surface patch), and a regular reparametrization is induced by a parameter diffeomorphism (Surface reparametrizations and their orientation sign).

[L2]

The chain rule gives Dψ=DφDh, and total derivatives applied to standard basis vectors are the parameter partial derivatives (The chain rule for total derivatives: D(gf)(a)=Dg(f(a))Df(a), A total derivative computes every directional derivative, and its matrix is the Jacobian).

Proof

technique · direct
1.1

By [L2], each of ψs and ψt is a linear combination of φu and φv at h(s,t), so the new tangent span is contained in the old one.

givenL1L2
2.1

Apply the same argument to the inverse parameter diffeomorphism h1; it expresses φu and φv as linear combinations of ψs and ψt, giving the reverse containment.

step 1.1L1L2
3.1

The two spans are equal. Invertibility of Dh ensures neither independent tangent pair loses rank.

step 1.1step 2.1
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A regular reparametrization of a connected parameter region has a constant orientation sign

Statement

Every regular reparametrization of a connected parameter region is either orientation-preserving everywhere or orientation-reversing everywhere.

Facts & Assumptions

Given: A regular reparametrization induced by a C1 diffeomorphism h between neighbourhoods of compact Jordan parameter regions whose interiors are nonempty and connected.

[L1]

If a C1 map has invertible derivative throughout a connected open set, then its Jacobian determinant is everywhere positive or everywhere negative (The Jacobian sign of a regular C1 map is constant on a connected domain).

[F1]

A reparametrization is orientation-preserving where detDh>0 and orientation-reversing where detDh<0 (Surface reparametrizations and their orientation sign).

Proof

technique · cases
1.1

Restrict h to the nonempty connected interior of the source region. Its derivative is invertible there, so [L1] gives a constant positive or negative determinant sign.

givenL1
2.1

Because the compact region is the closure of its interior and detDh is continuous and nonzero on a neighbourhood of it, the same strict sign holds on its boundary.

step 1.1given
3.1

In the positive case [assume-case pos], [F1] makes the reparametrization orientation-preserving everywhere; in the negative case [assume-case neg], [F1] makes it orientation-reversing everywhere. These cases exhaust [L1].

step 2.1F1cases-exhaustive
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The first fundamental form, Gram matrix, and area density of a surface patch

Definition

For a regular patch (D,φ) and an interior parameter point, whose tangent plane is defined by The tangent plane of a regular surface patch, put E=φu,φu,F=φu,φv,G=φv,φv. The matrix Gφ=(EFFG) is the Gram matrix of the parameter tangents, and the quadratic form Edu2+2Fdudv+Gdv2 is the first fundamental form (The Gram matrix G(v0,,vr1)=(vi,vj)i,j<r and Gram determinant, with empty value 1).

The surface area density is Jφ=detGφ, where Gφ is the Gram matrix of φu and φv. The determinant is nonnegative for all parameter points and positive in the interior because the two tangents are independent there (A Gram determinant is nonnegative and is positive exactly when the vector list is linearly independent), so the nonnegative square root exists and is unique.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The surface area density is the norm of the cross product of the parameter tangents

Statement

For every parameter point, Jφ=φu×φv2.

The common value is positive in the interior of a regular patch; it may vanish on the parameter boundary under the admitted seam and endpoint convention.

Facts & Assumptions

Given: A regular parametrized surface patch (D,φ).

[L1]

The density is the nonnegative square root of the determinant of the Gram matrix of φu,φv (The first fundamental form, Gram matrix, and area density of a surface patch).

[L2]

The determinant of a two-vector Gram matrix equals the squared cross-product norm (The squared cross-product norm is the Gram determinant of two vectors).

Proof

technique · direct
1.1

By [L1] and [L2], Jφ2=detGφ=φu×φv22.

givenL1L2
2.1

Both sides of the claimed equality are nonnegative, so uniqueness of the nonnegative square root gives Jφ=φu×φv2.

step 1.1algebra
3.1

Regularity makes the cross product nonzero in the interior, while the patch definition permits boundary zeros; this proves the qualification.

step 2.1
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

The oriented area vector transforms by the parameter Jacobian determinant

Statement

If ψ=φh, then ψs×ψt=(detDh)(φu×φv)h.

If ψ=φh, then Jψ=(Jφh)detDh.

Facts & Assumptions

Given: A regular reparametrization ψ=φh, with h=(h1,h2).

[L1]

The chain rule and the coordinate interpretation of total derivatives give ψs=(h1)s(φuh)+(h2)s(φvh) and the analogous formula for ψt (The chain rule for total derivatives: D(gf)(a)=Dg(f(a))Df(a), A total derivative computes every directional derivative, and its matrix is the Jacobian, Surface reparametrizations and their orientation sign).

Proof

technique · direct
1.1

Substitute the two formulas from [L1] into ψs×ψt. By [L2], the equal-vector terms vanish and the remaining terms combine to ((h1)s(h2)t(h2)s(h1)t)(φu×φv)h.

givenL1L2algebra
2.1

The scalar coefficient in step 1.1 is detDh, proving the signed area-vector formula.

step 1.1algebra
3.1

Taking Euclidean norms, using cw2=cw2, and applying [L2] gives Jψ=(Jφh)detDh.

step 2.1L2algebra
4.1

The first identity retains the determinant sign, while only the norm identity replaces it by an absolute value, as asserted.

step 2.1step 3.1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-24Open item page →

Surface area and scalar surface integrals on a regular patch

Definition

Let (D,φ) be a regular surface patch and let q be a continuous real-valued function on φ[D]. For a continuous scalar field q on the patch image, SqdS:=D(qφ)Jφ, and Area(S):=DJφ.

Here S denotes the patch with its chosen parametrization. Both integrands are bounded and Riemann integrable on the compact Jordan region D by continuity (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set). Boundary values are included in the parameter integral but may be changed on the content-zero boundary without changing its value.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Surface area and scalar surface integrals are invariant under regular reparametrization

Statement

Surface area and scalar surface integrals are unchanged by every regular reparametrization, regardless of orientation sign.

Facts & Assumptions

Given: A regular reparametrization ψ=φh from parameter region E onto parameter region D, and a continuous scalar field q on the common patch image.

[L1]

Scalar surface integrals are parameter integrals of (qφ)Jφ, and Jψ=(Jφh)detDh (Surface area and scalar surface integrals on a regular patch, The oriented area vector transforms by the parameter Jacobian determinant).

[L2]

Compact-Jordan change of variables gives E(kh)detDh=Dk for a neighbourhood diffeomorphism carrying E onto D (Change of variables for an injective C1 map on a compact Jordan set).

Proof

technique · direct
1.1

By [L1], the integral computed with ψ is E(qφh)(Jφh)detDh.

givenL1
2.1

Apply [L2] to k=(qφ)Jφ. The result is D(qφ)Jφ, the integral computed with φ.

step 1.1L2
3.1

The absolute determinant makes the calculation independent of orientation sign. Setting q=1 gives invariance of area.

step 2.1L1
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-24Open item page →

Unit normal fields, orientations, and flux through a regular surface patch

Definition

For a regular patch (D,φ), the parametrization induces on its interior the unit normal Nφ=φu×φvφu×φv2. The denominator is positive there by regularity and The surface area density is the norm of the cross product of the parameter tangents, and the vector is orthogonal to the tangent plane (The tangent plane of a regular surface patch). Choosing Nφ rather than Nφ is an orientation.

For a continuous vector field F, the flux in the orientation induced by φ is D(Fφ)(φu×φv). This is the scalar Riemann integral of a continuous function on D (Surface area and scalar surface integrals on a regular patch, The Euclidean inner product x,y=k<nxkyk on Rn); replacing the orientation by its negative negates the integrand.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Flux is invariant under orientation-preserving reparametrization and changes sign under reversal

Statement

An orientation-preserving reparametrization preserves flux and an orientation-reversing reparametrization negates it.

Facts & Assumptions

Given: A regular reparametrization ψ=φh between connected parameter regions and a continuous vector field F.

[L1]

Flux is the integral of Fφ dotted with the oriented area vector, and that vector transforms by the signed factor detDh (Unit normal fields, orientations, and flux through a regular surface patch, The oriented area vector transforms by the parameter Jacobian determinant).

[L2]

The determinant has one constant sign on the parameter region (A regular reparametrization of a connected parameter region has a constant orientation sign), and compact-Jordan change of variables uses detDh (Change of variables for an injective C1 map on a compact Jordan set).

Proof

technique · cases
1.1

By [L1], flux computed with ψ is E((Fφ)(φu×φv))hdetDh.

givenL1
2.1

In the preserving case [assume-case pos], [L2] gives detDh=detDh, so change of variables makes step 1.1 equal to the flux computed with φ.

step 1.1L2
2.2

In the reversing case [assume-case neg], [L2] gives detDh=detDh, so change of variables makes step 1.1 the negative of the flux computed with φ.

step 1.1L2
3.1

The two constant-sign cases are exhaustive, proving both assertions.

step 2.1step 2.2cases-exhaustive
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Content-zero parameter-boundary exceptions do not affect surface integrals

Statement

Changing a bounded scalar or flux parameter integrand only on the content-zero boundary of a compact Jordan parameter region preserves integrability and its integral.

In both directions, one of the two bounded functions is integrable if and only if the other is, and then their integrals agree.

Facts & Assumptions

Given: A compact Jordan parameter region D and bounded functions p,q:DR that agree on D.

[L2]

Bounded functions differing only on a content-zero set are integrable simultaneously and have equal integrals (Changing a bounded integrand on a content-zero set does not change its Riemann integral).

Proof

technique · direct
1.1

Since p=q on D, the set on which they differ is contained in DD=D, which has content zero by [L1].

givenL1
2.1

Apply [L2] to obtain both implications of the integrability equivalence and equality of the integrals.

step 1.1L2
3.1

A flux parameter integrand is scalar after taking the dot product, so the same argument applies to it. The conclusion licenses boundary seams, poles, and endpoint degeneracies only, not an interior rank failure.

step 2.1
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-24Open item page →

Finitely patched regular surfaces, their area, scalar integrals, and flux

Definition

A compatible finite patch presentation is a finite list of regular surface patches whose images cover a set S, such that for two distinct patches the preimage of their overlap has content zero in each parameter region. For flux, their induced normals must agree at every point of the overlap that is the image of an interior parameter point of both patches. Stating the requirement on the overlap itself is what gives it content: the induced normal of a patch is defined at the images of its interior parameter points, so a requirement imposed only away from the overlap preimages would constrain nothing and would admit opposite normals on patches whose interiors meet along a curve.

For a compatible finite patch presentation, area, scalar surface integrals, and oriented flux are the sums of the corresponding patch values; pairwise overlap preimages have content zero. The presentation is part of the data, so these sums are single-valued without presuming an unproved independence-of-presentation theorem. The content-zero modification result Content-zero parameter-boundary exceptions do not affect surface integrals ensures that seam, pole and endpoint values on a parameter boundary do not affect the individual summands. The content-zero condition on overlap preimages is a separate restriction on the presentation, and what it buys is that no piece of S carrying positive area is counted twice; each summand is an integral over the whole of its own parameter region and is unaffected by the overlaps.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Regular level surfaces have local regular parametrizations with the same tangent plane

Statement

Let F:UR3R be Ck, k1, and let c be a regular value. Every point of a regular level surface in R3 lies in the relative interior of a regular surface patch, and the patch tangent plane is the level-set tangent space.

If F1(c) is empty, the assertion is vacuous.

Facts & Assumptions

Given: The map F, regular value c, and a point pF1(c).

[L1]

Near p, the level is {p+u+g(u):uP} for a Ck map g on a neighbourhood P of 0 in K=kerDF(p) with g(0)=0 and Dg(0)=0, and dimK=2; a regular patch has nonzero parameter cross product in the interior and no interior parameter point shares its image with another point of the parameter region; its tangent plane is the span of the parameter derivatives (A regular level set is locally a Ck graph of dimension mn, The tangent space to a regular level set, Regular parametrized surface patches on compact Jordan parameter regions, The tangent plane of a regular surface patch).

[L2]

Equal-dimensional finite-dimensional vector spaces are linearly isomorphic, and partial derivatives are total derivatives applied to the standard coordinate vectors (Two finite-dimensional vector spaces over F are linearly isomorphic if and only if they have the same dimension, A total derivative computes every directional derivative, and its matrix is the Jacobian).

Proof

technique · direct
1.1

By [L1] write the level near p as p+u+g(u) for u near 0 in K, with Dg(0)=0. By [L2], choose a linear isomorphism L:R2K.

givenL1L2choose
2.1

Define φ(s,t)=p+L(s,t)+g(L(s,t)) and restrict it to a sufficiently small closed rectangle D about 0. The graph representation makes φ injective, and Dφ(0)=L has independent columns. By continuity, after shrinking the rectangle the parameter cross product stays nonzero in its interior, so [L1] makes (D,φ) a regular patch.

step 1.1L1L2construct
3.1

The image of Dφ(0) is K, so [L1] makes the patch tangent plane K and also identifies K with the level-set tangent space. Also p=φ(0) lies in the relative interior of the patch image.

step 2.1L1
4.1

The construction works at every point of a nonempty regular level, and there is nothing to choose or prove for an empty level.

step 3.1
CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

A compact regular level surface is covered by finitely many regular surface patches

Statement

If a regular level surface S=F1(c)R3 is compact, then finitely many regular surface patches have relative interiors whose union contains S. The empty surface is covered by the empty family.

Proof

technique · direct
1.1

If S=, the empty family covers it. Otherwise, for each pS, [L1] gives a patch whose relative interior contains p; these relative interiors form an open cover of S in its subspace topology.

givenL1
2.1

By [L2], select a finite subcover. The corresponding finite list of regular patches covers S.

step 1.1L2choose
3.1

Together with the empty case in step 1.1, this proves the statement for every compact regular level surface.

step 1.1step 2.1
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

Surface area, scalar integrals, and flux over a C1 graph

Statement

Let DR2 be a compact Jordan parameter region and let g be C1 on a neighbourhood of D. For the graph S={(x,y,g(x,y)):(x,y)D} and every continuous real-valued function q on S, Area(S)=D1+g22,SqdS=Dq(x,y,g(x,y))1+g22. For a continuous vector field F on S, upward flux is DF(x,y,g(x,y))(gx,gy,1). For the graph of g over D, the downward flux is the negative of DF(x,y,g(x,y))(gx,gy,1).

Facts & Assumptions

Proof

technique · direct
1.1

By [L1], φx×φy=(gx,gy,1), whose norm is 1+gx2+gy2=1+g22 and which never vanishes. The first two coordinates make φ injective, so it is a regular patch by [L2].

givenL1L2algebra
2.1

Substituting the norm from step 1.1 into the area and scalar-integral definitions in [L2] gives the first two formulas.

step 1.1L2
2.2

Retaining the signed vector from step 1.1 in the flux definition gives the upward formula; the downward orientation uses its negative and therefore negates the integral.

step 1.1L2
3.1

These substitutions establish all four displayed formulas, including the orientation distinction.

step 2.1step 2.2
TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24Open item page →

Scalar surface integrals on a surface of revolution

Statement

Let a<b, and let r:[a,b][0,) be C1 on a neighbourhood of [a,b], positive on (a,b), and allowed to vanish only at the endpoints. Put φ(s,t)=(s,r(s)cost,r(s)sint),(s,t)[a,b]×[0,2π]. For every continuous real-valued function q on φ([a,b]×[0,2π]), the scalar surface integral is SqdS=02πabq(φ(s,t))r(s)1+r(s)2dsdt, where S is the patch with its displayed parametrization.

Facts & Assumptions

Given: The nondegenerate interval, radius function, parametrization, and continuous scalar field q.

[L2]

A parametrization with nonzero cross product in the parameter interior and no interior parameter point sharing its image with another point of the region is a regular patch; its scalar integral uses the cross-product norm as density, and Jordan-Fubini identifies the rectangle integral with the stated iterated integral (Regular parametrized surface patches on compact Jordan parameter regions, The surface area density is the norm of the cross product of the parameter tangents, Surface area and scalar surface integrals on a regular patch, Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable).

Proof

technique · direct
1.1

By [L1], φs=(1,rcost,rsint) and φt=(0,rsint,rcost), and direct expansion gives φs×φt2=r(s)1+r(s)2.

givenL1algebra
2.1

In the rectangle interior, r(s)>0, so the cross product is nonzero. The first coordinate determines s, and the angle determines the point on the positive-radius circle for 0<t<2π; only the angular seam and possible endpoint-axis collapses lie on the boundary. Thus [L2] makes φ a regular patch.

givenstep 1.1L2
3.1

Substitute the density from step 1.1 into the scalar surface-integral definition and use the Jordan-Fubini clause in [L2] to obtain the stated iterated form.

step 1.1step 2.1L2
4.1

Endpoint zeros and the t=0,2π seam occur only on the content-zero parameter boundary, so they do not add terms or change the integral.

step 2.1step 3.1
CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-08-24Open item page →

The surface of revolution has area 2πabr(s)1+r(s)2ds

Statement

Assume the hypotheses of Scalar surface integrals on a surface of revolution. The surface obtained by rotating r about the axis has area 2πabr(s)1+r(s)2ds.

Facts & Assumptions

Given: A radius function satisfying the surface-of-revolution hypotheses.

[L1]

With scalar field q=1, the surface integral is 02πabr(s)1+r(s)2dsdt (Scalar surface integrals on a surface of revolution).

Proof

technique · direct
1.1

Set q=1 in [L1]. The inner integral is independent of t.

givenL1
2.1

Apply [L2] to integrate that constant inner value over 0t2π, obtaining the factor 2π and the displayed formula.

step 1.1L2
3.1

Possible endpoint zeros of r lie on the parameter boundary already covered by [L1], so no endpoint correction is present.

step 2.1L1

5 · Examples, counterexamples and false statements

None yet.

Sources