HasHodge

formal source

  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. -/
  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. -/
  42structure Medium (α : Type) [HasHodge α] where
  43  eps : ℝ
  44  mu  : ℝ
  45
  46/-- Sources (charge and current). -/
  47structure Sources (α : Type) where
  48  ρ : DForm α 0
  49  J : DForm α 1
  50
  51variable {α : Type}
  52
  53/-- Quasi-static Maxwell equations on the mesh (no time derivative terms).
  54    Faraday and Gauss-M are stated cleanly. Constitutive relations (const_D, const_B)
  55    and source equations (ampere_qs, gauss_e) require dimension n=3 for form-degree