IndisputableMonolith.MaxwellDEC

   1import Mathlib
   2
   3namespace IndisputableMonolith
   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. -/
  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
  56    alignment, so they are parameterized by the dimension hypothesis `hn`. -/
  57structure Equations (α : Type) [HasCoboundary α] [inst : HasHodge α] (M : Medium α) where
  58  E : DForm α 1
  59  H : DForm α 1
  60  B : DForm α 2
  61  D : DForm α 2
  62  src : Sources α
  63  /-- Faraday QS: curl E = 0 (no time-varying B in quasistatic limit) -/
  64  faraday_qs : HasCoboundary.d E = fun _ => 0
  65  /-- Ampere QS: d H = star J (requires n-1=2 for form-degree alignment) -/
  66  ampere_qs  : ∀ (hn : inst.n - 1 = 2),
  67    HasCoboundary.d H = cast (congrArg (DForm α) hn) (HasHodge.star src.J)
  68  /-- Gauss E: d D = star rho (requires n-0=3 for form-degree alignment) -/
  69  gauss_e    : ∀ (hn : inst.n - 0 = 3),
  70    HasCoboundary.d D = cast (congrArg (DForm α) hn) (HasHodge.star src.ρ)
  71  /-- Gauss M: div B = 0 (no magnetic monopoles) -/
  72  gauss_m    : HasCoboundary.d B = fun _ => 0
  73  /-- Constitutive: D = ε⋆E (requires n-1=2 for form-degree alignment) -/
  74  const_D    : ∀ (hn : inst.n - 1 = 2), D = hn ▸ (fun s => M.eps * HasHodge.star E s)
  75  /-- Constitutive: B = μ⋆H (requires n-1=2 for form-degree alignment) -/
  76  const_B    : ∀ (hn : inst.n - 1 = 2), B = hn ▸ (fun s => M.mu * HasHodge.star H s)
  77
  78/-- Pointwise Hodge energy density for 2-forms: ω · (⋆ω) on each 2-simplex.
  79    Requires n = 4 (spacetime dimension). -/
  80def energy2 (ω : DForm α 2) [inst : HasHodge α] (h : inst.n - 2 = 2) : DForm α 2 :=
  81  fun s => ω s * (h ▸ (HasHodge.star (k:=2) ω)) s
  82
  83/-- Admissibility: strictly positive material parameters. -/
  84def Admissible [HasHodge α] (M : Medium α) : Prop := 0 < M.eps ∧ 0 < M.mu
  85
  86/-- Positivity of the Hodge energy density for admissible media, provided the
  87    instance supplies `star2_psd`. This is signature-agnostic and delegates the
  88    sign choice to the instance via `star2_psd`. -/
  89theorem energy2_nonneg_pointwise
  90  [inst : HasHodge α] (h : inst.n - 2 = 2) (M : Medium α) (hadm : Admissible (α:=α) M) (ω : DForm α 2)
  91  : ∀ s, 0 ≤ energy2 (α:=α) ω h s := by
  92  intro s
  93  have hpsd := HasHodge.star2_psd (α:=α) h ω s
  94  simp [energy2]
  95  exact hpsd
  96
  97/-- PEC boundary descriptor (edges where tangential E vanishes). -/
  98structure PEC (β : Type) where
  99  boundary1 : Set (Simplex β 1)
 100
 101end MaxwellDEC
 102end IndisputableMonolith
 103