Admissible
plain-language theorem explainer
Admissible requires a medium to have strictly positive permittivity and permeability under the Hodge star interface. Discrete electromagnetism modelers cite this predicate to restrict constitutive relations to physical media. It is implemented as a direct conjunction of two inequalities on the eps and mu fields of the Medium structure.
Claim. A medium $M$ with permittivity $eps$ and permeability $mu$ is admissible if $eps > 0$ and $mu > 0$, given the Hodge star interface on the underlying type.
background
MaxwellDEC develops discrete exterior calculus for Maxwell equations on oriented simplices. The HasHodge class supplies the Hodge star operator with linearity, zero preservation, and the involution law star star x = signature(k) x that encodes metric signature effects. The Medium structure packages the two real scalars eps and mu for linear isotropic media.
proof idea
This is a direct definition that conjoins the two strict inequalities on the eps and mu fields of the Medium instance. No lemmas are applied.
why it matters
It supplies the positivity constraint referenced by BWD3Model for admissible linear witnesses and by ethical cost models for preference ordering. The definition supports discrete Maxwell systems by enforcing physical media parameters, consistent with Recognition Science requirements on positive constitutive coefficients and the Hodge star in D=3 settings.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.