PEC
plain-language theorem explainer
PEC encodes perfect electric conductor boundary conditions on a simplicial complex by recording the set of oriented edges where tangential electric field vanishes. Discrete exterior calculus treatments of Maxwell equations cite this record when imposing Dirichlet-type conditions on the 1-skeleton. The definition is a direct structure with a single field of type Set of oriented 1-simplices and requires no proof.
Claim. A perfect electric conductor boundary on a simplicial complex with vertex set $B$ is a subset of the oriented 1-simplices on which the tangential component of the electric 1-form is required to vanish.
background
The MaxwellDEC module constructs a discrete exterior calculus version of Maxwell's equations on oriented simplicial complexes. Its primitive object is the oriented k-simplex, an abstract identifier carrying an id of type α together with an orientation boolean. Discrete k-forms are then maps from these oriented simplices to values. The local setting is therefore a finite simplicial mesh equipped with the standard coboundary and Hodge operators of discrete exterior calculus.
proof idea
The declaration is a direct structure definition introducing the PEC record type with one field of type Set (Simplex β 1). No tactics or lemmas are applied.
why it matters
PEC supplies the boundary data consumed by energy2_nonneg_pointwise, which proves non-negativity of the Hodge energy density once an admissible medium and the star2_psd instance are given. In the Recognition Science setting this discrete energy positivity supports the passage from the forcing chain (T0-T8) to continuum Maxwell equations while preserving the phi-ladder mass spectrum and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.