Alphabeta Math
Physics theoremStatement: AI-adaptedProof: AI-adaptedPipeline-generated
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

Physical scope

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 U≅I×Ω of Laboratory geometry: a restricted inertial chart, its spatial slices and fixed-time fields: fields E,B:Ω×I→R3 jointly of class C1 with the additional derivatives required by each equation existing and continuous, and continuous source densities ρ,J of Charge parameter, frame charge and current densities, volume charge and flux, and the four-current. Let P,M and the derived objects ρb,Jb,ρf,Jf,D,H be those of Polarization, magnetization, bound and free sources, and the fields D and H, with P,M of class C2, and use the operators of Divergence and curl of a C1 vector field and Directional derivatives and partial derivatives of a map U⊆Rm→Rn. Then:

(a) [Bound-source conservation] ∂tρb+div⁡Jb=0 on Ω×I. Assume ACω (The Axiom of Countable Choice (ACω)) 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

∂tρf+div⁡Jf=∂tρ+div⁡J

as distributions on U, 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 ρ,J. Where the partial derivatives ∂tρ and ∂xiJi exist, the same identity holds pointwise by differentiating the free/bound decomposition; in particular, if these derivatives are continuous on U, both pairs satisfy the classical pointwise continuity equation. The bound-source conservation equation remains classical and uses only P,M∈C2.

(b) [Macroscopic equations] On Ω×I,

div⁡D=ρf,div⁡B=0,curl⁡E=−∂tB,curl⁡H=Jf+∂tD.

(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 E and B are unchanged, and the D and H equations hold for every C2 pair (P,M), independently of any constitutive law. The classical bound identity of (a) uses the exchange of ∂t with div⁡ for C2 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 (P,M); no constitutive relation and no empirical statement is made.

Facts & Assumptions

Given: The smooth-branch data of the Statement: E,B jointly C1 with the additional derivatives required by the adopted equations existing and continuous, continuous ρ,J, and jointly C2 model maps P,M with the derived objects ρb=−div⁡P, Jb=∂tP+curl⁡M, ρf=ρ−ρb, Jf=J−Jb, D=ε0E+P, H=μ0−1B−M 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 ACω (The Axiom of Countable Choice (ACω)).

[A1]

The adopted smooth-branch vacuum Maxwell equations: div⁡E=ρ/ε0, div⁡B=0, curl⁡E=−∂tB, curl⁡B=μ0J+c−2∂tE, 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)).

[L1]

The definition of the derived objects gives ρb=−div⁡P, Jb=∂tP+curl⁡M, ρ=ρf+ρb, J=Jf+Jb, D=ε0E+P and H=μ0−1B−M (Polarization, magnetization, bound and free sources, and the fields D and H, clauses (b)-(d)).

[L2]

If f is C2 on an open subset of Rm, then ∂i∂jf=∂j∂if there (Clairaut--Schwarz theorem for continuous second partial derivatives).

[L3]

The one-variable sum and scalar-multiple rules, f+g and αf differentiable with (f+g)′=f′+g′ and (αf)′=αf′, and the product rule, hold for differentiable real maps (Sums, scalar multiples, products and quotients: (f+g)′(c)=f′(c)+g′(c), (αf)′(c)=αf′(c), (fg)′(c)=f′(c)g(c)+f(c)g′(c), and (f/g)′(c)=(f′(c)g(c)−f(c)g′(c))/g(c)2 when g(c)≠0); partial derivatives are the one-variable derivatives of the line maps (Directional derivatives and partial derivatives of a map U⊆Rm→Rn), so these rules apply componentwise to the partial derivatives used below.

[L4]

Distributional derivatives satisfy ∂α∂βu=∂α+βu and ∂αuf=u∂αf for f∈Ck with ∣α∣≤k, under Countable Choice (Distributional differentiation is continuous and commutes); derivatives act by ⟨∂μT,ψ⟩=−⟨T,∂μψ⟩ (Distributional derivative), and the pairing is bilinear (Distribution).

[L5]

Locally integrable functions embed as regular distributions, uf(ψ)=∫fψ, 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).

[L6]

ε0=(μ0c2)−1, so 1/(c2ε0)=μ0 (Framework-local SI units, the vacuum constants and the exact/measured status of their values, clause (a)).

[L7]

One-coordinate integration by parts holds for C1 line restrictions on compact intervals (If u,v are differentiable on [a,b] with u′,v′ integrable, then ∫abuv′=u(b)v(b)−u(a)v(a)−∫abu′v); 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 U (Test function cutoffs and euclidean localization).

Proof

technique · direct substitution, distributional for the free/total identity and classical for the bound pair and the macroscopic equations
1.1A1L1L2L3

Compute ∂tρb+div⁡Jb=−∂tdiv⁡P+div⁡∂tP+div⁡curl⁡M by [L1], where the operators are those of [A1]'s conventions; the first two terms cancel because ∂tdiv⁡P=div⁡∂tP, and the last vanishes because div⁡curl⁡M=∑i,j,k=13εijk∂i∂jMk is an antisymmetrisation of the equal mixed partials ∂i∂jMk=∂j∂iMk; both identities are [L2] applied to the C2 components of P and M, and the algebra is [L3].

1.2A1L4L5L6

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 curl⁡B=μ0J+c−2∂tE of [A1]: the left side gives div⁡curl⁡B=∑i,j,kεijk∂i∂jBk=0 by the commutation of distributional derivatives [L4], while the right side gives μ0div⁡J+c−2∂tdiv⁡E with div⁡E=ρ/ε0 transferred by the classical-compatibility clause of [L4]; hence 0=μ0div⁡J+c−2ε0−1∂tρ=μ0(div⁡J+∂tρ) by [L6], so ∂tρ+div⁡J=0 as distributions, where ∂tρ and div⁡J denote the distributional derivatives of the regular distributions.

1.3A1L1L3L6

Compute the macroscopic equations: div⁡D=ε0div⁡E+div⁡P=ρ+div⁡P=ρ−ρb=ρf because ε0div⁡E=ρf+ρb and ρb=−div⁡P by [L1] and ρ=ρf+ρb by [L1]; div⁡B=0 and curl⁡E=−∂tB are the corresponding adopted equations of [A1] unchanged; and curl⁡H=μ0−1curl⁡B−curl⁡M=J+ε0∂tE−curl⁡M=Jf+∂t(ε0E+P)=Jf+∂tD, using [L1], μ0−1curl⁡B=μ0−1(μ0J+c−2∂tE)=J+(μ0c2)−1∂tE=J+ε0∂tE by [L6], and the decomposition J=Jf+∂tP+curl⁡M of [L1]; all identities are the componentwise algebra of [L3].

2.1step 1.1step 1.2L1L4

Subtract the distributional bound identity from the distributional total identity: by the decompositions of [L1] and the linearity of distributional differentiation [L4], ∂tρf+div⁡Jf=(∂tρ+div⁡J)−(∂tρb+div⁡Jb), 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 ∂tρf+div⁡Jf=∂tρ+div⁡J=0 as distributions on U, and the free pair is distributionally conserved exactly when the total pair is.

3.1step 1.1step 1.2step 1.3step 2.1L1L5L7∎

Suppose ∂tρ and ∂xiJi exist and are continuous on U. For a continuous scalar f with a continuous derivative in just one coordinate q, localize any test to rectangular boxes by [L7]. On each box, integration by parts on the q-lines has zero endpoint terms because the test vanishes there; Fubini then gives −∫f∂qψ=∫(∂qf)ψ. Summing the localized tests proves ∂quf=u∂qf without assuming derivatives in other coordinates. Apply this to (f,q)=(ρ,t) and (Ji,xi): the zero distribution of step 1.2 is the regular distribution of the continuous sum ∂tρ+∑i∂xiJi, which vanishes pointwise by [L5]. Since ρb,Jb are C1, the same argument applies to ρf,Jf 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

Dependency tree · 2 levels

Sources