DForm
plain-language theorem explainer
DForm α k is the type of real-valued functions on oriented k-simplices of a mesh α. Discrete exterior calculus implementations for Maxwell equations cite it as the carrier for cochains such as the electric and magnetic fields. The declaration is a direct one-line type abbreviation to Simplex α k → ℝ equipped with a simp attribute.
Claim. Let α be a type representing an abstract mesh. For each natural number k, the space of discrete k-forms consists of all maps from the set of oriented k-simplices to the real numbers.
background
The MaxwellDEC module constructs a discrete exterior calculus on an abstract mesh whose basic cells are given by the Simplex structure: each simplex carries an abstract identifier together with an orientation flag. Discrete k-forms are then defined as real-valued assignments to these oriented cells, supplying the cochain spaces on which the coboundary and Hodge operators act.
proof idea
The declaration is a direct type abbreviation: DForm α k expands to the function type Simplex α k → ℝ and carries the @[simp] attribute for automatic rewriting.
why it matters
DForm supplies the common carrier type for every discrete field appearing in the Equations structure (E, H, B, D) and in the energy2 density constructed via the Hodge star. It therefore underpins the entire discrete Maxwell system, including the constitutive relations and source terms that later feed into the Recognition Science derivation of electromagnetic constants and the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.