Sources
plain-language theorem explainer
The Sources structure packages charge density as a discrete 0-form ρ and current density as a discrete 1-form J on an oriented simplex mesh. Researchers assembling discrete exterior calculus models of electromagnetism cite it when building quasi-static Maxwell systems. The declaration is a direct structure definition that introduces the two fields with no further computation.
Claim. A source configuration on the discrete mesh consists of a charge density $ρ$ which is a real-valued function on oriented 0-simplices and a current density $J$ which is a real-valued function on oriented 1-simplices.
background
The MaxwellDEC module develops a discrete exterior calculus version of Maxwell's equations on an abstract oriented simplex mesh. DForm α k is the type of discrete k-forms, defined as the function type from oriented k-simplices to real numbers. Sources collects the inhomogeneous terms needed for the quasi-static regime: ρ for the charge contribution to Gauss's law and J for the current contribution to Ampere's law.
proof idea
This is a structure definition that directly declares the two fields ρ of type DForm α 0 and J of type DForm α 1. No lemmas or tactics are applied; the declaration serves as a data container.
why it matters
Sources supplies the source data required by the Equations structure in the same module, which is used by the levitation_is_inevitable theorem in AcousticPhaseLevitation. The definition supports the Recognition Science program of deriving electromagnetic behavior from the forcing chain by providing discrete charge and current terms that enter coherence-restoration calculations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.