Simplex
plain-language theorem explainer
The Simplex structure supplies an abstract oriented k-simplex consisting of an identifier of type α paired with a boolean orientation. Discrete exterior calculus work on Maxwell equations cites this when constructing discrete forms on meshes. The definition is a direct structure declaration with no lemmas or computational reduction.
Claim. An oriented $k$-simplex is a pair consisting of an abstract identifier $id$ of type $α$ and a boolean orientation flag $orient$.
background
In the MaxwellDEC module the basic objects for discrete exterior calculus are oriented simplices. The Simplex structure supplies the minimal data: an abstract label together with a choice of orientation. This matches the standard convention that discrete $k$-forms assign real values to oriented $k$-simplices, as seen in the sibling definition of DForm.
proof idea
The declaration is a direct structure definition that introduces exactly two fields. No lemmas from the upstream identity morphisms are invoked; the structure serves purely as a type constructor.
why it matters
This definition is the root type for the discrete exterior calculus layer. It is used by DForm to define discrete $k$-forms, by HasCoboundary to introduce the coboundary operator, by HasHodge to define the star operator, and by PEC to describe boundary conditions. The construction supports the translation of Maxwell equations into discrete operators while remaining compatible with the three-dimensional spatial structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.