Alphabeta MathLine Integrals and the Gradient Theorem
About this page
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.
✓ 22 results · all verified · 0 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 22 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
Linear Algebra
- Determinants of Matrices over a Commutative Ring
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Vector Spaces, Linear Subspaces, Span and Direct Sums
Real Analysis
- Arc Length and Rectifiable Curves
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Countability and Uncountability
- Foundations of the Real Numbers for Analysis
- Fubini and Change of Variables
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Properties of the Integral and the Working FTC
- 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
- Suprema and Infima
- The Derivative and the Mean Value Theorems
- The Fundamental Theorems of Calculus
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Total Derivative in ℝᵐ → ℝⁿ
- Topology of ℝ
Set Theory
2 · Logical flowchart
3 · Items
Definition
Reversal, concatenation, closed paths, and oriented piecewise-C1 reparametrizations
Definition
Scalar line integrals with respect to arc length and vector-field line integrals
Lemma
The piecewise-C1 line-integral sums do not depend on the admissible partition
Theorem
Scalar line integrals are parametrization-independent; vector line integrals retain orientation and change sign when it reverses
Theorem
Line integrals under reversal and concatenation
Theorem
Line-integral estimates by arc length and the supremum of the field
Corollary
The scalar line integral of one is the arc length
Corollary
For a C1 path the arc-length accumulation function has derivative equal to speed
Definition
Piecewise-C1 path-connected domains, potential functions, conservative fields, and path independence
Theorem
The gradient theorem: the line integral of a gradient is the endpoint increment
Corollary
Conservative fields are path-independent and have zero integral around every closed path
Theorem
Path independence is equivalent to zero integral around every closed piecewise-C1 path
Theorem
A continuous path-independent field has a potential constructed by line integrals
Theorem
Conservative, path-independent, and zero-closed-loop conditions are equivalent
Corollary
Two potentials of the same field differ by a constant on each piecewise-C1 path component
Lemma
Potentials glue after a constant adjustment over a nonempty path-connected overlap
Definition
Exact and closed C1 vector fields
Lemma
Continuous second partials of a scalar potential commute
Theorem
Every exact C1 vector field is closed
Definition
Star-shaped open subsets of Euclidean space
Theorem
Poincare's lemma on a star-shaped domain: every closed C1 field is exact
Corollary
On a star-shaped open domain, closed, exact, conservative, path-independent, and zero-loop are equivalent
Definition
Type I, Type II, and elementary regions for Green's theorem
Definition
Positive orientation of elementary-region boundaries
Lemma
The Type I boundary identity for the P dx term
Lemma
The Type II boundary identity for the Q dy term
Lemma
Shared boundary arcs cancel when finitely many elementary regions are glued
Theorem
Green's theorem for finite unions of elementary regions
Corollary
Area of an elementary Green region as a boundary line integral
Remark
Limitation: arbitrary Jordan domains are not covered by the elementary Green theorem
Remark
Closedness is local, exactness is global, and a domain hypothesis cannot be omitted
Sources
- J. Lebl, Basic Analysis II, sections 9.2 and 9.3
- J. Lebl, Basic Analysis II, section 9.2
- J. Lebl, Basic Analysis II, Proposition 9.2.15
- J. Lebl, Basic Analysis II, Proposition 9.2.10
- J. Lebl, Basic Analysis II, section 9.3
- J.-B. Campesato, Poincare Lemma, sections 1 and 2
- J. Lebl, Basic Analysis II, Theorem 9.3.1
- J. Lebl, Basic Analysis II, Corollary 9.3.2
- J. Lebl, Basic Analysis II, Theorem 9.3.3
- J.-B. Campesato, Poincare Lemma, section 1
- J.-B. Campesato, Poincare Lemma, section 2
- J. Lebl, Basic Analysis II, section 10.6
- J. Lebl, Basic Analysis II, Theorem 10.6.1