structure
definition
Medium
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.MaxwellDEC on GitHub at line 42.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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