Medium
plain-language theorem explainer
Medium packages the two real scalars eps and mu that define a linear isotropic medium on any type alpha carrying a Hodge star. Mesh-based electromagnetism codes and discrete Maxwell solvers cite this when supplying constitutive relations for a given mesh geometry. The declaration is a plain structure definition with no computational content or proof obligations.
Claim. A linear medium on a space or mesh $alpha$ equipped with a Hodge star is specified by two real scalars $varepsilon$ (permittivity) and $mu$ (permeability).
background
The MaxwellDEC module works with differential forms on oriented simplices. The HasHodge class supplies the Hodge star operator that maps k-forms to (n-k)-forms, together with linearity axioms and the involution law star star = sigma(k) id, where sigma encodes the metric signature (for example (-1)^{k(4-k)} in 4D Riemannian geometry). The sibling Sources structure holds the charge density rho as a 0-form and the current J as a 1-form. Upstream the mu definition in Cost.Ndim.Projector extracts the scalar coefficient from the quadratic relation A squared equals mu A.
proof idea
The declaration is a structure definition that directly introduces the two fields eps and mu; no lemmas or tactics are applied.
why it matters
This structure supplies the constitutive interface used by the Admissible predicate (which requires eps greater than 0 and mu greater than 0) and by the Equations that encode the quasi-static Maxwell system on the mesh. It appears in downstream flight and chemistry modules as the material model for energy and thrust calculations. In the Recognition framework it supplies the metric-dependent part of the discrete Maxwell equations on 3D meshes, consistent with T8 (D equals 3) and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.