HasHodge
The Hodge star interface class equips a simplicial mesh with a linear operator mapping k-forms to (n-k)-forms while enforcing a signature-scaled double-star involution. Researchers building discrete Maxwell systems cite it to encode constitutive relations between field pairs. The declaration is a direct class definition that bundles the linearity axioms and involution law without further proof steps.
claimA type α admits a Hodge star operator when equipped with a natural number n and maps ⋆ from DForm(α,k) to DForm(α,n-k) that are additive, homogeneous, zero-preserving, and satisfy ⋆⋆x = σ(k)x for a signature function σ, together with a positivity condition on 2-forms when n=4.
background
The MaxwellDEC module develops discrete exterior calculus on abstract simplicial complexes. An oriented k-simplex pairs an identifier from α with a boolean orientation. A discrete k-form assigns a real value to each such simplex. The Hodge star interface supplies the metric-dependent operator that pairs field strengths with fluxes, abstracting constitutive relations in the discrete setting. It draws on the simplicial ledger identification of discrete operators with continuum limits via weighted edge sums.
proof idea
The declaration is a class definition. Its fields directly encode the star map together with the algebraic requirements for linearity, zero preservation, and the signature-adjusted involution. No lemmas or tactics are applied; the structure itself constitutes the interface.
why it matters in Recognition Science
The interface is required by the Medium structure for linear material parameters and by the Equations structure for quasi-static Maxwell on the mesh. It supports the energy2 definition for 2-form energy density and the nonnegativity result for admissible media. In the Recognition framework it supplies the constitutive law for the discrete Maxwell system, consistent with the forcing chain that fixes three spatial dimensions while allowing general n for spacetime formulations.
scope and limits
- Does not construct an explicit metric on the simplices.
- Does not prescribe a concrete form for the signature function.
- Does not restrict the dimension n to three.
- Does not include time derivatives or full dynamic terms.
formal statement (Lean)
25class HasHodge (α : Type) where
26 n : Nat
27 star : ∀ {k : Nat}, DForm α k → DForm α (n - k)
28 star_add : ∀ {k} (x y : DForm α k), star (fun s => x s + y s) = (fun s => star x s + star y s)
29 star_zero : ∀ {k}, star (fun (_ : Simplex α k) => 0) = (fun _ => 0)
30 star_smul : ∀ {k} (c : ℝ) (x : DForm α k), star (fun s => c * x s) = (fun s => c * (star x s))
31 signature : Nat → ℝ
32 star_star : ∀ {k} (h : n - (n - k) = k) (x : DForm α k),
33 h ▸ (star (star x)) = (fun s => signature k * x s)
34 /-- Optional positivity control on 2-forms (useful in 4D Riemannian media).
35 Requires n = 4 so that star maps 2-forms to 2-forms.
36 Instances targeting Lorentzian signatures can simply provide a trivial
37 proof such as `by intro; intro; exact le_of_eq (by ring)` if not used. -/
38 star2_psd : ∀ (h : n - 2 = 2) (x : DForm α 2) (s : Simplex α 2),
39 0 ≤ x s * (h ▸ (star x)) s
40
41/-- Linear medium parameters. -/