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 macroscopic Maxwell equations in terms of D, H and the free sources
The macroscopic Maxwell equations div D=rho_f, div B=0, curl E=-d_tB, curl H=J_f+d_tD, together with the conservation of the bound source pair, as a conditional consequence of the adopted smooth vacuum equations and the bound/free decomposition, for C^2 macroscopic dipole densities on the laboratory region. No constitutive law, no weak-branch or singular-source claim and no empirical statement. Free/total conservation is distributional for the continuous-source class under AC_omega, and classical under the stated additional source derivatives.
Statement
Assume the smooth branch of the vacuum Maxwell postulate The microscopic vacuum Maxwell equations: smooth and weak branches on the laboratory region of Laboratory geometry: a restricted inertial chart, its spatial slices and fixed-time fields: fields jointly of class with the additional derivatives required by each equation existing and continuous, and continuous source densities of Charge parameter, frame charge and current densities, volume charge and flux, and the four-current. Let and the derived objects be those of Polarization, magnetization, bound and free sources, and the fields D and H, with of class , and use the operators of Divergence and curl of a vector field and Directional derivatives and partial derivatives of a map . Then:
(a) [Bound-source conservation] on . Assume (The Axiom of Countable Choice ()) for the regular-distribution and classical-compatibility interfaces below. Identify continuous sources with their regular distributions using Regular distribution from a locally integrable function and Locally integrable functions embed in distributions. Then
as distributions on , with derivatives as in Distributional derivative: the free pair is distributionally conserved exactly when the total pair is. Under the adopted four vacuum equations both sides are zero distributions, by Distributional differentiation is continuous and commutes. These statements do not require classical derivatives of . Where the partial derivatives and exist, the same identity holds pointwise by differentiating the free/bound decomposition; in particular, if these derivatives are continuous on , both pairs satisfy the classical pointwise continuity equation. The bound-source conservation equation remains classical and uses only .
(b) [Macroscopic equations] On ,
(c) [Interpretation and scope] Equations (b) are an exact rewriting of the adopted vacuum equations under the decomposition of Polarization, magnetization, bound and free sources, and the fields D and H: the two equations written in and are unchanged, and the and equations hold for every pair , independently of any constitutive law. The classical bound identity of (a) uses the exchange of with for data; the free/total identity is distributional in the stated continuous-source class, with its classical interpretation only under the additional derivatives stated in (a). The distributional conservation conclusion embeds the adopted smooth solution only; no macroscopic field-equation claim is made for the weak branch of the Maxwell postulate, for singular or sheet sources or for discontinuous ; no constitutive relation and no empirical statement is made.
Facts & Assumptions
Given: The smooth-branch data of the Statement: jointly with the additional derivatives required by the adopted equations existing and continuous, continuous , and jointly model maps with the derived objects , , , , , of Polarization, magnetization, bound and free sources, and the fields D and H, on the laboratory region of Laboratory geometry: a restricted inertial chart, its spatial slices and fixed-time fields with the units of Framework-local SI units, the vacuum constants and the exact/measured status of their values. Assume (The Axiom of Countable Choice ()).
The adopted smooth-branch vacuum Maxwell equations: , , , , with the divergence and curl of the named vector-calculus definition and the partial derivative of the named partial-derivative definition, as fixed in the Statement (The microscopic vacuum Maxwell equations: smooth and weak branches, clause (a)).
The definition of the derived objects gives , , , , and (Polarization, magnetization, bound and free sources, and the fields D and H, clauses (b)-(d)).
If is on an open subset of , then there (Clairaut--Schwarz theorem for continuous second partial derivatives).
The one-variable sum and scalar-multiple rules, and differentiable with and , and the product rule, hold for differentiable real maps (Sums, scalar multiples, products and quotients: , , , and when ); partial derivatives are the one-variable derivatives of the line maps (Directional derivatives and partial derivatives of a map ), so these rules apply componentwise to the partial derivatives used below.
Distributional derivatives satisfy and for with , under Countable Choice (Distributional differentiation is continuous and commutes); derivatives act by (Distributional derivative), and the pairing is bilinear (Distribution).
Locally integrable functions embed as regular distributions, , and this identification is injective on continuous functions: a continuous function whose regular distribution vanishes is identically zero (Regular distribution from a locally integrable function, Locally integrable functions embed in distributions).
One-coordinate integration by parts holds for line restrictions on compact intervals (If are differentiable on with integrable, then ); their continuous products have the same Riemann and Lebesgue integrals (A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral). Fubini applies to the resulting compactly supported integrable products (Fubini's theorem for L^1 functions on a sigma-finite product); smooth partitions localize tests to rectangular boxes compactly contained in (Test function cutoffs and euclidean localization).
Proof
Compute by [L1], where the operators are those of [A1]'s conventions; the first two terms cancel because , and the last vanishes because is an antisymmetrisation of the equal mixed partials ; both identities are [L2] applied to the components of and , and the algebra is [L3].
Identify the continuous fields and sources with their regular distributions by [L5] and apply the distributional divergence of [L4] to the adopted Ampere-Maxwell identity of [A1]: the left side gives by the commutation of distributional derivatives [L4], while the right side gives with transferred by the classical-compatibility clause of [L4]; hence by [L6], so as distributions, where and denote the distributional derivatives of the regular distributions.
Compute the macroscopic equations: because and by [L1] and by [L1]; and are the corresponding adopted equations of [A1] unchanged; and , using [L1], by [L6], and the decomposition of [L1]; all identities are the componentwise algebra of [L3].
Subtract the distributional bound identity from the distributional total identity: by the decompositions of [L1] and the linearity of distributional differentiation [L4], , the second summand is the regular distribution of the continuous function shown to vanish in step 1.1, and the first is the zero distribution by step 1.2; hence as distributions on , and the free pair is distributionally conserved exactly when the total pair is.
Suppose and exist and are continuous on . For a continuous scalar with a continuous derivative in just one coordinate , localize any test to rectangular boxes by [L7]. On each box, integration by parts on the -lines has zero endpoint terms because the test vanishes there; Fubini then gives . Summing the localized tests proves without assuming derivatives in other coordinates. Apply this to and : the zero distribution of step 1.2 is the regular distribution of the continuous sum , which vanishes pointwise by [L5]. Since are , the same argument applies to and gives their classical continuity equation. Steps 1.1, 1.3 and 2.1 establish the remaining claims and their stated model-conditional scope.
Depends on
Euclidean maps and diffeomorphisms
Directional derivatives and partial derivatives of a map
Divergence and curl of a vector field
The electric and magnetic fields as fixed-time spatial vector fields
Laboratory geometry: a restricted inertial chart, its spatial slices and fixed-time fields
Polarization, magnetization, bound and free sources, and the fields D and H
Framework-local SI units, the vacuum constants and the exact/measured status of their values
Charge parameter, frame charge and current densities, volume charge and flux, and the four-current
The microscopic vacuum Maxwell equations: smooth and weak branches
Sums, scalar multiples, products and quotients: , , , and when
Clairaut--Schwarz theorem for continuous second partial derivatives
The Axiom of Countable Choice ()
Distribution
Distributional derivative
Regular distribution from a locally integrable function
Locally integrable functions embed in distributions
Distributional differentiation is continuous and commutes
If are differentiable on with integrable, then
Fubini's theorem for L^1 functions on a sigma-finite product
Test function cutoffs and euclidean localization
A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral
Dependency tree · 2 levels
Sources
- David Tong, Electromagnetism, University of Cambridge Part II Mathematical Tripos lecture notes (2026 printing, 236 pp.)
- David J. Griffiths, Introduction to Electrodynamics, 3rd edition (Prentice Hall 1999, 596 pp.; full scanned text)
- R. Fitzpatrick, Electromagnetism (University of Texas at Austin course), node 73: Magnetization