A Duality-Invariant Extended Action for Nonlinear Partially Massless Spin Two

We construct a local covariant extended action for the full nonlinear spin-two partially massless Dirac-Born-Infeld equations of Cherney, Deser, Waldron and Zahariade. Two independent rank-two auxiliary fields pair with the constitutive divergence and the dual curvature divergence. All original equations follow from auxiliary variations, and every original solution lifts with zero auxiliary fields. The density is invariant off shell under the original infinitesimal nonlinear duality, extended by rotation of the auxiliary pair. Equality of physical degrees of freedom and a global finite-duality construction are not claimed. The deposit contains the manuscript PDF, LaTeX sources, Lean proofs and audit logs, and symbolic checks. The Lean development verifies continuous-integral projection and explicit constitutive calculations. Its geometric and analytic assumptions and the separately computed de Sitter counterexample are distinguished in the manuscript and theorem map. Version 1.1 — core verification supplement, 28 October 2026. A fresh verification passed 56/56 build targets and audited 171 public theorems. The core proves actual integral variation and exact extended-action recovery of the complete nonlinear spin-two constitutive divergence and covariant curl equations on the actual de Sitter flat-slicing patch and the original D>0 real branch, under the hypotheses in SCOPE and the theorem map. A global de Sitter atlas/action is outside this supplement. These counts do not certify the manuscript as a whole: in particular, they are not a completed Lean verification of the full action’s duality invariance, arbitrary-coordinate/frame covariance, every supplementary discussion or search classification, physical degrees-of-freedom equivalence, or bibliographic priority. Use PMDBI_Duality_Core_Verification_Scope_20261028.pdf and PMDBI_Duality_Core_Lean_Verification_20261028.zip for the current formal scope. The original manuscript and earlier source package are retained unchanged. AI tools were used to assist Lean code development and verification, translation, and to accelerate multiplier searches and tests.