energy2
plain-language theorem explainer
Pointwise Hodge energy density for a discrete 2-form on a four-dimensional mesh is supplied by multiplying the form value by its Hodge dual at each simplex. Discrete Maxwell codes cite it when assembling the quadratic energy term. The body is a one-line wrapper that multiplies the form value by the starred value after the dimension cast.
Claim. For a discrete 2-form $ω$ on a mesh of dimension 4, the energy density is the map sending each 2-simplex $s$ to the product $ω(s) · (⋆ω)(s)$, where ⋆ is the Hodge star supplied by the metric interface.
background
A discrete k-form assigns a real scalar to each oriented k-simplex. The HasHodge class supplies a Hodge star operator mapping k-forms to (n-k)-forms, together with linearity axioms and an involution law controlled by a signature function that encodes the metric. This module develops a discrete exterior calculus for Maxwell equations on simplicial meshes, with the Hodge star encoding constitutive relations of the medium.
proof idea
This is a one-line wrapper that applies the pointwise product of the 2-form with its Hodge star after the dimension cast supplied by the equality hypothesis.
why it matters
It is invoked by the non-negativity theorem for admissible media. The definition supplies the quadratic energy term inside the discrete Maxwell system, where the Hodge star implements the constitutive map. It supports the discrete analog of the electromagnetic action in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.