Maxwell Dec

Discrete electromagnetic bookkeeping

Maxwell's equations describe how electric and magnetic fields behave. Traditionally they are written with derivatives and integrals over continuous space. Maxwell DEC is a way to write the same physics on a discrete mesh: a collection of points, edges, faces, and volumes. Instead of fields at every point, you record values on these geometric pieces. The name DEC stands for discrete exterior calculus, the branch of mathematics that does calculus on such meshes.

The module defines the basic objects. A simplex is the abstract name for a point, edge, triangle, or tetrahedron, with an orientation, a choice of which direction counts as positive. A discrete k-form is a real number assigned to each oriented k-simplex: a 0-form assigns numbers to points, a 1-form to edges, a 2-form to faces, and so on. The coboundary operator d takes a k-form to a (k+1)-form, generalizing the gradient, curl, and divergence. The Hodge star converts between forms of complementary degree, and it carries the metric information, such as the signature of spacetime. A medium is a pair of numbers, the permittivity eps and permeability mu, which describe how the material responds to electric and magnetic fields.

On top of these, the module states the quasi-static Maxwell equations, the version with no time derivatives. In plain language, they say: the electric field has no curl, the magnetic field has no divergence, and the sources (charge and current) are related to the fields through the medium. The equations are written with the coboundary and Hodge star, so they hold on any mesh that satisfies the required dimension conditions. The module also defines the energy density stored in a 2-form, which represents the electromagnetic field in four dimensions.

The main theorem is a positivity result. If the medium is admissible, meaning both eps and mu are strictly positive, then the pointwise energy density is nonnegative at every face. This is proved in the machine-checked library of formal theorems. The proof uses a property called star2_psd, which the Hodge star instance must supply. That property is the discrete analogue of the statement that the energy of a physical field cannot be negative. The theorem is signature-agnostic: it works for both Riemannian and Lorentzian metrics, because the sign choice is delegated to the instance.

What this establishes is a guarantee. In the discrete setting, if you start with an admissible medium and a Hodge star that satisfies the positivity condition, then the energy computed on every face is never negative. This is the discrete version of a fundamental physical requirement. It means the discrete formulation is not just a formal game; it respects the energy bound that continuous electromagnetism obeys. The module provides the vocabulary and the proof skeleton for doing electromagnetic calculations on a mesh with confidence.

/-- Positivity of the Hodge energy density for admissible media, provided the
    instance supplies `star2_psd`. This is signature-agnostic and delegates the
    sign choice to the instance via `star2_psd`. -/
theorem energy2_nonneg_pointwise
  [inst : HasHodge α] (h : inst.n - 2 = 2) (M : Medium α) (hadm : Admissible (α:=α) M) (ω : DForm α 2)
  : ∀ s, 0 ≤ energy2 (α:=α) ω h s := by
  intro s
  have hpsd := HasHodge.star2_psd (α:=α) h ω s
  simp [energy2]
  exact hpsd

/-- Positivity of the Hodge energy density for admissible media, provided the
    instance supplies `star2_psd`. This is signature-agnostic and delegates the
    sign choice to the instance via `star2_psd`. -/
theorem energy2_nonneg_pointwise
  [inst : HasHodge α] (h : inst.n - 2 = 2) (M : Medium α) (hadm : Admissible (α:=α) M) (ω : DForm α 2)
  : ∀ s, 0 ≤ energy2 (α:=α) ω h s := by
  intro s
  have hpsd := HasHodge.star2_psd (α:=α) h ω s
  simp [energy2]
  exact hpsd

What this page does not claim

The module does not define a specific Hodge star instance for any particular metric. It does not prove existence or uniqueness of solutions to the discrete Maxwell equations. It does not address time-dependent Maxwell equations; only the quasi-static case is stated.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/MaxwellDEC.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: