A Local Extended Action for Tensorial Superspace Equations with Verified Component Recovery

This preprint constructs a local extended action for the complete free tensorial superspace equations D_[mu D_nu] Phi = 0, retaining all symmetric tensorial coordinates and Grassmann components. The original superfield is real and total-even; the total number of original and external odd generators is even. An explicit auxiliary-field coefficient map gives a real scalar action as the real part of the joint Grassmann top coefficient integrated over the bosonic coordinates. The accompanying Lean 4.19.0 / mathlib v4.19.0 sources prove the actual continuous first variation, integration by parts, the computed local adjoint, the complete real-even Euler system, and both recovery directions: every stationary extended configuration projects to an original solution, and every original solution has a stationary zero-auxiliary lift. A separate fresh-source compilation and axiom audit is included. Scope: this is an adjoint-field variational embedding. Full OSp(1|2n) covariance of the extended action, equivalence to stationarity of the entire external-Grassmann-valued action, and equality of physical degrees of freedom are not established. The paper therefore does not claim to settle the stronger symmetry-preserving physical missing-action problem. The record contains the paper PDF, LaTeX source, Lean proofs, theorem map, build instructions and audit reports. The known adjoint-field construction is credited; the contribution is its explicit application and verified continuum recovery for the stated field space. AI assistance was used for Lean code development and verification, translation, and accelerated multiplier searches and tests.