IndisputableMonolith.MaxwellDEC
MaxwellDEC module introduces the oriented k-simplex as abstract identifier and the surrounding discrete exterior calculus structures for Maxwell equations in the Recognition Science setting. It defines Simplex, DForm, coboundary, Hodge, medium, sources and equations on simplicial complexes. The module is purely definitional.
claimThe module defines the oriented $k$-simplex (abstract identifier) together with differential forms, coboundary and Hodge operators on simplicial complexes for the discrete Maxwell system.
background
The module sits in the MaxwellDEC domain and imports only Mathlib. Its sibling definitions introduce the basic objects: oriented $k$-simplex, $D$-form, the HasCoboundary and HasHodge type classes, Medium, Sources, Equations, and the energy and admissibility predicates. The local theoretical setting is the translation of classical electromagnetism into discrete exterior calculus on abstract simplicial complexes.
proof idea
This is a definition module, no proofs.
why it matters in Recognition Science
The module supplies the discrete geometric primitives required to state Maxwell's equations and the associated energy functional inside the Recognition Science framework. No downstream theorems are recorded yet.