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.
Regular Surfaces and Surface Integrals
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Binary Operations, Monoids, Groups and Subgroups
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Connectedness
- Constant Rank, Submersions, Immersions and Regular Level Sets
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Determinants of Matrices over a Commutative Ring
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Fubini and Change of Variables
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Improper and Parameter-Dependent Multiple Integrals
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Simple Field Extensions and the Construction of the Complex Numbers
- Sine, Cosine, and the Definition of Pi
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Vector Spaces, Linear Subspaces, Span and Direct Sums
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
The cross product in
Definition
For and in , define .
This is the right-handed cross product. The displayed coordinates are those of the standard basis (The standard list with and for is an ordered basis of ; hence , and is the zero space with basis and dimension ), and inner products and norms are those of The Euclidean inner product on .
The cross product is bilinear, alternating, and orthogonal to both factors
Statement
For all , the cross product is bilinear and alternating, , and is orthogonal to both and .
Facts & Assumptions
Given: Vectors and a scalar .
The cross product is given by its three coordinate differences of products (The cross product in ), and the Euclidean inner product is the coordinate dot product (The Euclidean inner product on ).
The determinant of a real matrix is its signed permutation sum (For , the determinant over a commutative ring by the Leibniz formula, and for a real matrix).
Proof
Substitution in [L1] gives , , and the corresponding two identities in the second argument.
The same coordinate formula gives and , so the product is alternating.
Expanding the dot product in [L1] yields , which is the determinant by [L2].
Taking or makes the determinant have two equal columns and hence zero; therefore is orthogonal to both factors. The calculation includes zero and parallel vectors.
The squared cross-product norm is the Gram determinant of two vectors
Statement
For , , and this value is positive exactly when and are linearly independent.
Equivalently,
Facts & Assumptions
Given: Vectors .
The cross product has the displayed coordinate formula, and it is bilinear, alternating, and orthogonal to its factors (The cross product in , The cross product is bilinear, alternating, and orthogonal to both factors).
The two-vector Gram matrix has entries , and its determinant is positive exactly for a linearly independent pair and zero exactly for a dependent pair (The Gram matrix and Gram determinant, with empty value , A Gram determinant is nonnegative and is positive exactly when the vector list is linearly independent).
Proof
Expanding the three squared coordinates of and collecting terms gives .
The right side of step 1.1 is , which is by [L2].
The positivity and vanishing assertions follow from [L2], including the cases in which either vector is zero.
Regular parametrized surface patches on compact Jordan parameter regions
Definition
A compact Jordan parameter region is a compact Jordan measurable set that is the closure of its nonempty connected interior (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 is Jordan measurable iff its boundary is null, equivalently of content zero).
A regular parametrized surface patch is the image of a 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 is the Euclidean componentwise class of Euclidean maps and diffeomorphisms. More precisely, the parametrization is defined on an open neighbourhood of , on , and no point of has the same image as a distinct point of . The chosen pair is part of the patch data.
The tangent plane of a regular surface patch
Definition
Let be a regular parametrized surface patch (Regular parametrized surface patches on compact Jordan parameter regions) and let with . At an interior parameter point, the tangent plane is .
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 (Linear combination of a finite list, and the span as the smallest linear subspace containing ). The affine tangent plane through is .
Surface reparametrizations and their orientation sign
Definition
Let and be regular surface patches. A regular reparametrization from to is a diffeomorphism between neighbourhoods of their compact Jordan parameter regions with . We additionally require ( Euclidean maps and diffeomorphisms).
The derivative is invertible, so its Jacobian determinant is nonzero (The Jacobian determinant of a square-dimensional 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.
The tangent plane is invariant under regular reparametrization
Statement
Regular reparametrizations preserve the tangent plane at corresponding interior parameter points.
Precisely, if and is interior, then
Facts & Assumptions
Given: A regular reparametrization and an interior parameter point .
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).
The chain rule gives , and total derivatives applied to standard basis vectors are the parameter partial derivatives (The chain rule for total derivatives: , A total derivative computes every directional derivative, and its matrix is the Jacobian).
Proof
By [L2], each of and is a linear combination of and at , so the new tangent span is contained in the old one.
Apply the same argument to the inverse parameter diffeomorphism ; it expresses and as linear combinations of and , giving the reverse containment.
The two spans are equal. Invertibility of ensures neither independent tangent pair loses rank.
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 diffeomorphism between neighbourhoods of compact Jordan parameter regions whose interiors are nonempty and connected.
If a 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 map is constant on a connected domain).
A reparametrization is orientation-preserving where and orientation-reversing where (Surface reparametrizations and their orientation sign).
Proof
Restrict to the nonempty connected interior of the source region. Its derivative is invertible there, so [L1] gives a constant positive or negative determinant sign.
Because the compact region is the closure of its interior and is continuous and nonzero on a neighbourhood of it, the same strict sign holds on its boundary.
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].
The first fundamental form, Gram matrix, and area density of a surface patch
Definition
For a regular patch and an interior parameter point, whose tangent plane is defined by The tangent plane of a regular surface patch, put The matrix is the Gram matrix of the parameter tangents, and the quadratic form is the first fundamental form (The Gram matrix and Gram determinant, with empty value ).
The surface area density is , where is the Gram matrix of and . 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.
The surface area density is the norm of the cross product of the parameter tangents
Statement
For every parameter point, .
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 .
The density is the nonnegative square root of the determinant of the Gram matrix of (The first fundamental form, Gram matrix, and area density of a surface patch).
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
By [L1] and [L2], .
Both sides of the claimed equality are nonnegative, so uniqueness of the nonnegative square root gives .
Regularity makes the cross product nonzero in the interior, while the patch definition permits boundary zeros; this proves the qualification.
The oriented area vector transforms by the parameter Jacobian determinant
Statement
If , then .
If , then .
Facts & Assumptions
Given: A regular reparametrization , with .
The chain rule and the coordinate interpretation of total derivatives give and the analogous formula for (The chain rule for total derivatives: , A total derivative computes every directional derivative, and its matrix is the Jacobian, Surface reparametrizations and their orientation sign).
The cross product is bilinear and alternating (The cross product is bilinear, alternating, and orthogonal to both factors), and area density is the cross-product norm (The surface area density is the norm of the cross product of the parameter tangents).
Proof
Substitute the two formulas from [L1] into . By [L2], the equal-vector terms vanish and the remaining terms combine to .
The scalar coefficient in step 1.1 is , proving the signed area-vector formula.
Taking Euclidean norms, using , and applying [L2] gives .
The first identity retains the determinant sign, while only the norm identity replaces it by an absolute value, as asserted.
Surface area and scalar surface integrals on a regular patch
Definition
Let be a regular surface patch and let be a continuous real-valued function on . For a continuous scalar field on the patch image, , and .
Here denotes the patch with its chosen parametrization. Both integrands are bounded and Riemann integrable on the compact Jordan region 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.
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 from parameter region onto parameter region , and a continuous scalar field on the common patch image.
Scalar surface integrals are parameter integrals of , and (Surface area and scalar surface integrals on a regular patch, The oriented area vector transforms by the parameter Jacobian determinant).
Compact-Jordan change of variables gives for a neighbourhood diffeomorphism carrying onto (Change of variables for an injective map on a compact Jordan set).
Proof
By [L1], the integral computed with is .
Apply [L2] to . The result is , the integral computed with .
The absolute determinant makes the calculation independent of orientation sign. Setting gives invariance of area.
Unit normal fields, orientations, and flux through a regular surface patch
Definition
For a regular patch , the parametrization induces on its interior the unit normal 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 rather than is an orientation.
For a continuous vector field , the flux in the orientation induced by is . This is the scalar Riemann integral of a continuous function on (Surface area and scalar surface integrals on a regular patch, The Euclidean inner product on ); replacing the orientation by its negative negates the integrand.
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 between connected parameter regions and a continuous vector field .
Flux is the integral of dotted with the oriented area vector, and that vector transforms by the signed factor (Unit normal fields, orientations, and flux through a regular surface patch, The oriented area vector transforms by the parameter Jacobian determinant).
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 (Change of variables for an injective map on a compact Jordan set).
Proof
By [L1], flux computed with is .
In the preserving case [assume-case pos], [L2] gives , so change of variables makes step 1.1 equal to the flux computed with .
In the reversing case [assume-case neg], [L2] gives , so change of variables makes step 1.1 the negative of the flux computed with .
The two constant-sign cases are exhaustive, proving both assertions.
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 and bounded functions that agree on .
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
Since on , the set on which they differ is contained in , which has content zero by [L1].
Apply [L2] to obtain both implications of the integrability equivalence and equality of the integrals.
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.
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 , 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 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.
Regular level surfaces have local regular parametrizations with the same tangent plane
Statement
Let be , , and let be a regular value. Every point of a regular level surface in lies in the relative interior of a regular surface patch, and the patch tangent plane is the level-set tangent space.
If is empty, the assertion is vacuous.
Facts & Assumptions
Given: The map , regular value , and a point .
Near , the level is for a map on a neighbourhood of in with and , and ; 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 graph of dimension , 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).
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 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
By [L1] write the level near as for near in , with . By [L2], choose a linear isomorphism .
Define and restrict it to a sufficiently small closed rectangle about . The graph representation makes injective, and has independent columns. By continuity, after shrinking the rectangle the parameter cross product stays nonzero in its interior, so [L1] makes a regular patch.
The image of is , so [L1] makes the patch tangent plane and also identifies with the level-set tangent space. Also lies in the relative interior of the patch image.
The construction works at every point of a nonempty regular level, and there is nothing to choose or prove for an empty level.
A compact regular level surface is covered by finitely many regular surface patches
Statement
If a regular level surface is compact, then finitely many regular surface patches have relative interiors whose union contains . The empty surface is covered by the empty family.
Facts & Assumptions
Given: A compact regular level surface .
Every point of lies in the relative interior of a regular surface patch (Regular level surfaces have local regular parametrizations with the same tangent plane).
Compactness is intrinsic to the subspace metric, and every open cover of a compact metric space has a finite subcover (A subset of a metric space is open in the subspace metric exactly when it is the trace of an open set of the ambient space, and it is compact as a metric space in its own right exactly when every family of open subsets of the ambient space covering it, indexed or not, has finitely many members covering it, Open cover, subcover, compact metric space, and compact subset of a metric space).
Proof
If , the empty family covers it. Otherwise, for each , [L1] gives a patch whose relative interior contains ; these relative interiors form an open cover of in its subspace topology.
By [L2], select a finite subcover. The corresponding finite list of regular patches covers .
Together with the empty case in step 1.1, this proves the statement for every compact regular level surface.
Surface area, scalar integrals, and flux over a graph
Statement
Let be a compact Jordan parameter region and let be on a neighbourhood of . For the graph and every continuous real-valued function on , For a continuous vector field on , upward flux is For the graph of over , the downward flux is the negative of .
Facts & Assumptions
Given: The region , function , graph parametrization , continuous scalar field , and continuous vector field .
Derivative algebra and the gradient definition give and (Sums, scalar multiples, products and quotients: , , , and when , The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case).
A nonzero parameter cross product gives a regular patch, area density is its norm, and scalar integrals and flux use the corresponding parameter integrands (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, Unit normal fields, orientations, and flux through a regular surface patch).
Proof
By [L1], , whose norm is and which never vanishes. The first two coordinates make injective, so it is a regular patch by [L2].
Substituting the norm from step 1.1 into the area and scalar-integral definitions in [L2] gives the first two formulas.
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.
These substitutions establish all four displayed formulas, including the orientation distinction.
Scalar surface integrals on a surface of revolution
Statement
Let , and let be on a neighbourhood of , positive on , and allowed to vanish only at the endpoints. Put For every continuous real-valued function on , the scalar surface integral is where is the patch with its displayed parametrization.
Facts & Assumptions
Given: The nondegenerate interval, radius function, parametrization, and continuous scalar field .
The sine and cosine derivative formulas and derivative algebra compute the parameter tangents, and (The derivatives of sine and cosine are cosine and minus sine, Sums, scalar multiples, products and quotients: , , , and when , Parity and the Pythagorean identity for sine and cosine).
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
By [L1], and , and direct expansion gives .
In the rectangle interior, , so the cross product is nonzero. The first coordinate determines , and the angle determines the point on the positive-radius circle for ; only the angular seam and possible endpoint-axis collapses lie on the boundary. Thus [L2] makes a regular patch.
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.
Endpoint zeros and the seam occur only on the content-zero parameter boundary, so they do not add terms or change the integral.
The surface of revolution has area
Statement
Assume the hypotheses of Scalar surface integrals on a surface of revolution. The surface obtained by rotating about the axis has area .
Facts & Assumptions
Given: A radius function satisfying the surface-of-revolution hypotheses.
With scalar field , the surface integral is (Scalar surface integrals on a surface of revolution).
Jordan-Fubini separates a continuous integrand on a rectangle, and the integral of the constant over is (Fubini over a bounded Jordan set when all but a content-zero family of sections are integrable, If on then for every partition ; in particular every constant function is integrable, with ).
Proof
Set in [L1]. The inner integral is independent of .
Apply [L2] to integrate that constant inner value over , obtaining the factor and the displayed formula.
Possible endpoint zeros of lie on the parameter boundary already covered by [L1], so no endpoint correction is present.
5 · Examples, counterexamples and false statements
None yet.
Sources
- M. E. Taylor, Introduction to Analysis in Several Variables, Section 3.2
- University of Toronto MAT237 notes, Section 5.3
- M. E. Taylor, Introduction to Analysis in Several Variables, formulas 3.2.18-3.2.20
- R. Sjamaar, Manifolds and Differential Forms, Theorem 8.4
- University of Toronto MAT237 notes, Section 5.3, An Invariance Property
- M. E. Taylor, Introduction to Analysis in Several Variables, formulas 3.2.7-3.2.13
- R. Sjamaar, Manifolds and Differential Forms, Section 8.1
- M. E. Taylor, Introduction to Analysis in Several Variables, formula 3.2.12
- University of Toronto MAT237 notes, Section 5.3, Piecewise Smooth Surfaces
- J. M. Lee, Introduction to Smooth Manifolds, Regular Level Set Theorem
- M. E. Taylor, Introduction to Analysis in Several Variables, formulas 3.2.21-3.2.23
- University of Toronto MAT237 notes, Section 5.3, Special Cases
- M. E. Taylor, Introduction to Analysis in Several Variables, Exercise 17
- APEX Calculus II, Section 7.4