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.
Sourced Maxwell sign and current conservation — Examples
1 · Prerequisites
- Abelian Categories
- Absolute and Conditional Convergence; Rearrangement; Products
- Binary Operations, Monoids, Groups and Subgroups
- Categories, Functors and Natural Transformations
- Chain Complexes and Homology
- Cm Math Continuum
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Connectedness
- Connections And Free Fall
- Connections Levi Civita and Parallel Transport
- 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
- Countability Axioms and Cardinal Functions
- Curvature And Tides
- 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
- Einstein And Matter
- Euclidean Ordinary Differential Equations with Smooth Dependence
- Exterior Powers, Orientation and Hodge Duality
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Framework And Geometry
- Free Modules, Exact Sequences, Projective and Injective Modules
- Fubini and Change of Variables
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Geodesics, the Exponential Map, Completeness, and Hopf–Rinow
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Hereditary and Productive Behaviour of the Separation Axioms
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Improper and Parameter-Dependent Multiple Integrals
- Improper Integrals
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Limits and Colimits
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Manifolds with Boundary Collars and Orientations
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- 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
- Oriented Lorentzian fields, observers and coordinate conventions
- Picard-Lindelöf and First-Order Ordinary Differential Equations
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Preadditive and Additive Categories and Biproducts
- Properties of the Integral and the Working FTC
- Rank Theorems and Embedded Submanifolds
- Relations, Functions, and Quotients
- Riemann Curvature and Riemannian Submanifolds
- Riemannian Metrics Length Distance and Volume
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Separation Axioms: the Hierarchy
- 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
- Simplicial Complexes and Simplicial Homology
- Sine, Cosine, and the Definition of Pi
- Singular Chains and Singular Homology
- Singular Cochains Mayer Vietoris and Smooth Singular Comparison
- Singular Cohomology and Coefficient Theorems
- Smooth Manifolds and Smooth Maps
- Smooth Partitions of Unity and Exhaustions
- Smooth Vector Bundles and Sections
- Sourced Maxwell sign and current conservation
- Spacetime Primitives
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- Tangent Cotangent and the Differential
- Tensor Fields Exterior Algebra and Differential Forms
- Tensor Products of Modules
- Tensors And Observers
- The de Rham Theorem and Degree
- The Derivative and the Mean Value Theorems
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- The Divergence Theorem and Classical Stokes
- The Exponential Function
- The Exterior Derivative and Cartan Calculus
- The Fundamental Theorems of Calculus
- The Inverse and Implicit Function Theorems
- The Inverse Function Theorem Completed
- The Logarithm and General Powers
- 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 Fields Flows and Lie Derivatives
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Volumes of Elementary Solids and Solids of Revolution
2 · Summary
Scope
This companion gives an explicit smooth Maxwell field and current on a flat product with compact spatial three-torus. The equations hold pointwise, while the total charge on the compact boundaryless spatial cycle vanishes. The construction is a mathematical model example, not a reported experiment or a claim about a physical system.
3 · Logical flowchart
4 · Definitions, postulates, theorems and proofs
None yet.
5 · Examples, experiments and counterexamples
Compact boundaryless Gauss neutrality
Example
Fix periods and use the smooth quotient geometry and global forms and vector fields supplied by The scaled three-torus as a smooth compact flat spatial manifold. In its coordinates set , with , orientation , and time orientation . Fix as real coefficients and put
These lifts on are independent of and are -periodic. Let be their unique smooth descents, so and . The descended global vector field satisfies and . On the lifts, and . Define the smooth current and field
Let be the slice inclusion , and let Orient the slice by the restriction of the global form . Let be the affine identification . Let be the oriented spatial slice , represented as a finite smooth singular chain as follows. Triangulate the fundamental cube by the six tetrahedra indexed by . The ordered vertices of tetrahedron are , , , and . Let be the affine map taking to these ordered vertices; it extends affinely to . Define the smooth singular simplex ; in the standard parameter it satisfies . It extends smoothly to a neighborhood of in its affine plane because extends affinely and are smooth. Put . Thus each simplex maps into the slice of . The determinant of the ordered edge vectors is , so this coefficient gives each simplex the cube orientation. The six regions are the orderings of ; their interiors are disjoint and their union is the cube. Internal faces cancel in pairs, and opposite cube faces are identified by period translations with opposite boundary orientations, as verified below.
The perspective box depicts the fundamental cube, with opposite faces paired by the labels. Its dotted body diagonal is the shared edge of the six affine tetrahedra indexed by coordinate permutations. The drawing is schematic and is not used in the chain-boundary proof above.
Facts & Assumptions
Given: , the product Lorentzian geometry and the smooth fields in the Example.
The scaled three-torus as a smooth compact flat spatial manifold proves the quotient is a smooth compact boundaryless torus, the global descend, and on the product the metric components are constant , the Christoffel symbols vanish, and .
The alternating current-flux form is and charge is (The metric volume form, current flux through 3-faces and finite-chain charges, Gauss charge and finite-chain flux balance).
For any finite smooth singular three-cycle on which a smooth sourced Maxwell field is defined, the Gauss lemma Gauss charge and finite-chain flux balance gives zero total charge.
The smooth tangent-bundle conventions inherited from Oriented Lorentzian fields, observers and coordinate conventions and Gauss charge and finite-chain flux balance use ; the finite torus chain below is explicit and uses no additional choice (The Axiom of Countable Choice ()).
The boundary of an ordered smooth singular -simplex is the alternating sum of its four face maps, and the boundary of a finite chain is the finite sum of these boundaries (Smooth singular chain and cochain complexes).
The power-series definitions and convergence, followed by repeated termwise differentiation, make and smooth. Their first derivatives are and , and both have period (Sine and cosine defined by their real power series, The sine and cosine power series converge absolutely for every real argument, Inside its radius a real power series may be differentiated term by term, and the differentiated series has the same radius, The derivatives of sine and cosine are cosine and minus sine, The zero sets of sine and cosine and the least positive common period 2 pi).
The chain rule gives on the lift; hence for the descended functions. The continuous lift derivative is Riemann integrable, and its integral equals the endpoint difference of (The chain rule for total derivatives: , A continuous function on is Riemann integrable, by Heine-Cantor and Riemann's criterion, The lower and upper Darboux integrals of a bounded on as and , Darboux integrability as their equality, and the notation , The second fundamental theorem: if is differentiable on with and is integrable, then ).
The published definition Integral of a form over a smooth singular simplex defines the integral of a smooth -form over a smooth singular -simplex as the Jordan-set Riemann integral of the coefficient of its pullback in the standard positive affine coordinates on ; it also establishes that is compact Jordan. The published, audited change-of-variables theorem Change of variables for an injective map on a compact Jordan set states: if is open, is injective and with invertible throughout , and is compact Jordan, then for bounded the two integrability conditions are equivalent and, when they hold, Its proof also establishes compact Jordan status of .
The published boundary criterion says a Euclidean-metric-bounded set is Jordan measurable exactly when its boundary has content zero (A bounded set in is Jordan measurable iff its boundary is null, equivalently of content zero). The published graph theorem says the graph of a continuous function on a closed nondegenerate rectangle has content zero (The graph of a continuous function on a closed nondegenerate rectangle in has content zero in ). The published compact-Jordan integrability theorem states that a continuous function on a compact Jordan set is integrable there (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set), and closed bounded subsets of are compact (Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line). Content zero passes to subsets and finite unions because a subset inherits a finite cube cover and finitely many such covers can be combined (Measure zero and content zero in by countable and finite cube covers). If bounded Jordan sets fill a bounded Jordan set up to a content-zero remainder, have pairwise content-zero intersections, and a bounded function is integrable on and every , then the published finite-additivity lemma Additivity of the integral over finitely many Jordan pieces that fill a Jordan set up to content zero gives .
The published theorem Every continuous function on a closed nondegenerate rectangle in is Riemann integrable says every continuous real function on a closed nondegenerate rectangle in is Riemann integrable. The published rectangular Fubini theorem Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections says that for an integrable function on a product of nondegenerate rectangles, the iterated section integrals exist when the sections in that order are integrable and equal the multiple integral. The published multidimensional Darboux definition The lower and upper Darboux integrals over a nondegenerate rectangle in gives the common lower/upper sum value when they agree, and rectangle volume is the product of side lengths by the published definition Axis-parallel rectangles in and their volume; in particular, a constant on a rectangle has integral because each lower and upper Darboux sum has that value.
Verification
Given: [F1]–[F10], the geometry, fields and finite chain defined in the Example.
For a fixed permutation , the barycentric coordinates of a point in the ordered region relative to its four listed vertices are , , , and ; these are nonnegative, sum to one, and reconstruct the point. Thus the six tetrahedra cover the cube with disjoint interiors. Each extends affinely to , so extends smoothly to the affine plane containing and is a smooth singular simplex into . The ordered edge determinant is , so the weight orients each tetrahedron by .
The periodic lifts are smooth by [F6], and their descents are smooth by the torus lemma; [F6]–[F7] give , so and are smooth global fields on the product. Since , , the homogeneous equation holds. Raising indices gives and . Thus , , and the equations have both sides zero. Thus both field equations are verified everywhere.
An internal facet arises by setting one adjacent-coordinate inequality to equality. The two permutations differ by swapping those adjacent entries; their omitted vertices occupy the same position in the ordered vertex lists, and the remaining three vertices have the same order. Thus the face maps in [F5] are identical, while the permutation signs are opposite. Their two coefficients in the signed face boundary therefore sum to zero. This covers both internal facet types (equal first and second coordinates, or equal second and third coordinates).
Fix a coordinate and order the other two indices as . The triangle on comes from permutation by omitting vertex ; its ordered vertices are , , and . The triangle on comes from by omitting the final vertex; its ordered vertices are , , and . Translation by makes these vertex lists identical, so their quotient face maps are equal. Moving from first to last is two transpositions, so the permutation coefficients agree; the omitted-vertex boundary signs are and . By [F5] the corresponding face terms cancel. This pairs every outer triangle, for all three coordinates and both orders .
Let and let be the affine tetrahedron with the ordered vertices specified in the Example; each is closed and bounded, hence compact by [F9], so the continuous lift is bounded there. The standard is compact Jordan by [F8]. Write for the affine parametrization already defined. The standard positive parameterization of is . Since and by [F1], the interior-product definition in [F2] gives . The pullback of by has coefficient in the standard positive affine coordinates, because pulls back the descended spatial coordinate forms to the Euclidean coordinate forms and restricts them to the slice [F1]. By [F8] this is the coefficient whose integral defines . This coefficient is continuous on compact Jordan , hence integrable by [F9]. The determinant of the three edge vectors is , so the chain coefficient gives The last equality is [F8]'s change-of-variables formula: is compact Jordan, extends to an injective affine map on with nonsingular constant derivative, and is bounded and continuous on . The cube and each are closed and bounded, hence compact by Heine--Borel, and they are bounded Jordan sets. Indeed their boundaries are finite unions of bounded pieces of affine planes; each such piece is contained in the graph of an affine function over a containing closed nondegenerate rectangle after solving the plane equation for a coordinate with nonzero normal component. These graphs have content zero by [F9], so the boundary criterion in [F9] applies. By step 1.1 the six cover and have disjoint interiors. Thus each pairwise intersection is contained in the union of their boundaries and has content zero by finite-union and subset closure in [F9], while the remainder is empty. The coefficient is continuous and bounded on the compact Jordan sets , so all integrals in the finite additivity hypotheses are defined by [F9]. Applying the finite Jordan-set additivity result in [F9] and using the chain definition in [F2] gives
The finite chain boundary is the alternating face sum in [F5]. Steps 2.1 and 2.2 cancel every internal and external face term, respectively. Hence , as required in [F3]. The explicit finite triangulation adds no choice, as [F4] records.
Since by step 3.1, the finite-chain neutrality result [F3] applies and gives .
Write and , so . The lift is continuous on and hence integrable there by [F10]. Rectangular Fubini [F10] applies, and its sections over are the constant function . The multidimensional Darboux sums and volume formula in [F10] therefore give By [F7], and the one-dimensional FTC gives , since the sine values at and agree. Hence the direct integral computation also yields , in agreement with step 4.1.
Remarks
This is a mathematical model with smooth fields. It illustrates the compact-cycle constraint without using a point source or a boundary at infinity; it does not report a measurement or assert that the model describes nature.