A Local Differential-Multiplier Action for an Isotropic Skewon Medium

A local differential-multiplier action is constructed for the source-free isotropic skewon constitutive model D = epsilon E + sigma B and H = mu⁻¹ B + sigma E, with real constant epsilon > 0, mu > 0 and sigma nonzero. Solving the compatibility equations for second-order spatial differential multipliers and integrating the resulting expressions gives a local action in the four ordinary electromagnetic potentials, without auxiliary fields. The action contains additional spatial derivatives. Its stationary equations are equivalent to all Maxwell equations, including Gauss constraints, in the declared smooth H6/L2 class over a finite time interval and all of space. The action and genuine first variations have a common continuum mesh limit. The accompanying Lean 4.19.0/mathlib development verifies the actual operators, spacetime integral, first variation, both recovery directions and continuum limits. All 91 compilation units passed, and 942 local theorem roots passed a recursive dependency audit using only standard Lean logical axioms. Reproducible source files, build records, source hashes and the audit are included. This is a result for the specified constant isotropic sector, not for an arbitrary fifteen-component skewon or unrestricted boundary conditions. The skewon contribution still cancels from the usual constitutive chi FF expression; the present action uses a broader derivative structure. No priority claim is made. The deposit contains the manuscript PDF, LaTeX sources and full Lean verification package. AI tools assisted Lean formalization and checking, translation, and accelerated multiplier searches and tests.