pith. machine review for the scientific record. sign in
structure definition def or abbrev

Equations

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  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). -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (14)

Lean names referenced from this declaration's body.