Simplex

formal source

   4namespace MaxwellDEC
   5
   6/-- Oriented k-simplex (abstract id). -/
   7structure Simplex (α : Type) (k : Nat) where
   8  id     : α
   9  orient : Bool
  10
  11/-- Discrete k-form: value per oriented k-simplex. -/
  12@[simp] def DForm (α : Type) (k : Nat) := Simplex α k → ℝ
  13
  14/-- Coboundary operator interface on the mesh. -/
  15class HasCoboundary (α : Type) where
  16  d : ∀ {k : Nat}, DForm α k → DForm α (k+1)
  17  d_zero : ∀ {k}, d (fun (_ : Simplex α k) => 0) = (fun _ => 0)
  18
  19/-- Hodge star interface (metric/constitutive).
  20    We expose linearity and a signature-correct involution law `⋆⋆ = σ(k) · id`.
  21    The `σ` function captures the metric signature effect; for example in 4D
  22    Riemannian one may take `σ k = (-1)^(k*(4-k))`, while in Lorentzian (−,+,+,+)
  23    one would use `σ k = (-1)^(k*(4-k)+1)`. We keep this abstract so concrete
  24    meshes can choose either. -/
  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. -/