A Local Displacement-Only Action for an Odd-Mass Continuum Model

A local finite-derivative action is constructed for a specified two-dimensional homogeneous, nondispersive odd-mass continuum with equal diagonal inertial coefficients and nonzero antisymmetric off-diagonal mass. Direct pairing and all constant recombinations fail in the stated parameter range. Solving compatibility equations for a spatial differential multiplier and integrating the resulting derivatives produces an action involving only the original two displacement fields, without auxiliary fields. Stationarity is equivalent to both original equations in the declared smooth H6/L2 class over a finite time interval and the full plane. The associated 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 125 compilation units passed, and 1,239 local theorem roots passed a recursive dependency audit using only standard Lean logical axioms. The package includes reproducible sources, build records, source hashes and the audit. The result does not change the antisymmetric mass tensor’s zero contribution to the conventional quadratic kinetic energy, does not identify the action with the device’s stored physical energy, and does not represent the complete frequency-dependent experimental device of Wu et al. (PNAS 120, e2209829120, 2023). The accessible main article does not explicitly pose a missing-generalized-action problem. The present work addresses the stated continuum model and makes no claim of priority or unrestricted-boundary equivalence. 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.