Maxwell Dec Sources

Sources

In the discrete setting of the framework's machine-checked library of formal theorems, a source is a pair of fields: charge density ρ, a value assigned to each oriented point (a 0-simplex), and current density J, a value assigned to each oriented edge (a 1-simplex). The declaration Sources packages exactly these two pieces of data. It is a structure, not a theorem: it defines what a source is, not what it does.

The declaration sits inside a broader formalization of discrete exterior calculus, where fields live on a mesh of simplices rather than on a continuum. The same file defines the coboundary operator d, which generalizes grad, curl, and div, and the Hodge star, which encodes the metric or constitutive relations. These are the tools the quasistatic Maxwell equations use to connect sources to fields: Ampère's law reads d H = ⋆ J and Gauss's law reads d D = ⋆ ρ, both stated in the Equations structure. The Sources declaration itself only supplies the data those equations consume.

The declaration makes no claim about physics. It does not assert that charge is conserved, that sources are physical, or that the equations hold. It does not fix the dimension of space or the signature of the metric; those choices live in the HasHodge instance and the dimension hypothesis hn passed to Equations. The structure is deliberately minimal: two fields, one on points and one on edges, with no additional constraints.

What the declaration does establish is a vocabulary. It gives a name and a shape to the abstract notion of a source in discrete electromagnetism, so that later theorems and definitions can refer to it. It is a definitional choice, a piece of the framework's language, not a result about the world.

/-- Sources (charge and current). -/
structure Sources (α : Type) where
  ρ : DForm α 0
  J : DForm α 1

/-- Sources (charge and current). -/
structure Sources (α : Type) where
  ρ : DForm α 0
  J : DForm α 1

What this page does not claim

The Sources declaration does not prove any physical law, such as conservation of charge. It does not fix the dimension or signature of spacetime; those choices are made elsewhere. It does not state the Maxwell equations themselves, which live in the Equations structure.

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: