energy2_nonneg_pointwise
plain-language theorem explainer
energy2_nonneg_pointwise establishes that the pointwise Hodge energy density on 2-forms remains non-negative at every simplex once the HasHodge instance supplies its star2_psd axiom. Discrete exterior calculus workers modeling electromagnetic fields on meshes cite the result to guarantee local positivity of their quadratic energy forms. The tactic proof is a direct reduction: it invokes star2_psd at an arbitrary simplex and simplifies the energy2 definition to match.
Claim. Let $n=4$ and let a Hodge star instance on the mesh be given. For any admissible medium and any discrete 2-form $ω$, the pointwise energy density $ω(s) · (⋆ω)(s)$ satisfies $ω(s) · (⋆ω)(s) ≥ 0$ at every oriented 2-simplex $s$.
background
DForm α k is the type of discrete k-forms: real-valued assignments to oriented k-simplices. HasHodge α is the class supplying the Hodge star operator ⋆ together with linearity, an involution law ⋆⋆ = σ(k) id, and the optional star2_psd axiom that asserts non-negativity of the 2-form pairing ω · (⋆ω) when n=4. Medium α packages the constitutive scalars eps and mu; Admissible requires both to be strictly positive. The module MaxwellDEC develops a discrete exterior calculus treatment of Maxwell equations on abstract meshes, with energy2 defined as the pointwise product ω(s) · (⋆ω)(s) under the dimension witness h : n-2=2.
proof idea
The proof introduces an arbitrary simplex s, obtains the non-negativity claim directly from HasHodge.star2_psd instantiated at s, simplifies the definition of energy2, and closes the goal by exact matching.
why it matters
The result secures local positivity of the quadratic energy induced by the Hodge star on 2-forms, a prerequisite for stability of discrete electromagnetic schemes. It supplies the pointwise non-negativity step inside the MaxwellDEC development; no downstream uses are recorded yet. In the Recognition framework it aligns with the requirement that energy densities derived from the J-cost remain non-negative.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.