Sources
plain-language theorem explainer
Sources records charge density as a discrete 0-form and current as a discrete 1-form on an abstract simplex mesh. Workers assembling discrete Maxwell systems in the Recognition framework cite this record when stating the inhomogeneous equations. The declaration is a bare structure definition that simply packages the two fields with no further axioms or proofs.
Claim. Let $DForm(α, k)$ be the space of discrete $k$-forms, i.e., real-valued assignments to each oriented $k$-simplex of the mesh $α$. Then Sources$(α)$ is the structure whose fields are a discrete 0-form $ρ$ (charge density) and a discrete 1-form $J$ (current density).
background
The MaxwellDEC module treats oriented $k$-simplices as abstract identifiers for mesh elements. DForm $α$ $k$ is defined as the function type from Simplex $α$ $k$ to $ℝ$, supplying the concrete type for discrete forms. Sources collects the two inhomogeneous source terms required by the quasi-static Maxwell system on this mesh.
proof idea
The declaration is a structure definition with two fields and no proof body or lemmas applied.
why it matters
Equations in the same module uses Sources to package the full quasi-static system, while levitation_is_inevitable in AcousticPhaseLevitation invokes it when assembling the coherence certificate that derives acoustic levitation from gravity-as-coherence. The structure therefore supplies the source terms that link discrete electromagnetism to the Recognition forcing chain and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.