Sources
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.
claimA 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 in Recognition Science
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.
scope and limits
- Does not include time derivatives or full dynamic evolution.
- Does not specify medium parameters eps and mu.
- Does not assume a concrete mesh dimension.
- Does not encode boundary conditions or topological data.
formal statement (Lean)
47structure Sources (α : Type) where
48 ρ : DForm α 0
49 J : DForm α 1
50
51variable {α : Type}
52
53/-- Quasi-static Maxwell equations on the mesh (no time derivative terms).
54 Faraday and Gauss-M are stated cleanly. Constitutive relations (const_D, const_B)
55 and source equations (ampere_qs, gauss_e) require dimension n=3 for form-degree
56 alignment, so they are parameterized by the dimension hypothesis `hn`. -/