HasCoboundary
plain-language theorem explainer
The HasCoboundary class equips an abstract type alpha with a coboundary operator that raises the degree of discrete forms by one while preserving the zero section. Workers assembling discrete exterior calculus models for electromagnetism cite this interface when building the mesh-level Maxwell system. The declaration is a type class definition that directly states the operator family and its zero axiom.
Claim. A type $alpha$ carries a coboundary operator when there exists a map $d$ sending each discrete $k$-form (a real-valued function on oriented $k$-simplices) to a discrete $(k+1)$-form, with the property that $d$ applied to the zero form yields the zero form.
background
The module introduces oriented $k$-simplices as abstract identifiers carrying an orientation flag. A discrete $k$-form on such a mesh is simply a real-valued assignment to each oriented simplex. The local setting therefore treats the mesh as a combinatorial object on which differential operators can be defined without reference to an embedding space.
proof idea
This is a type class definition that declares the coboundary map $d$ together with the single axiom that it sends the zero section to itself.
why it matters
The class is required by the Equations structure that assembles the quasi-static Maxwell system, stating Faraday and Gauss laws together with constitutive relations on the mesh. It supplies the discrete differential structure needed to embed electromagnetism into the Recognition framework's algebraic setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.