A Local Extended Action for κ(R,T) Gravity with Exact Projected Recovery

A local extended action is constructed for the full κ(R,T) metric equations, with a smooth arbitrary coupling and a prescribed constitutive source T[g,χ]. The dependence of the source, its trace, curvature and volume density is retained in the variation; no division by κ is used. The Lean 4.19.0 / mathlib v4.19.0 development proves the actual continuous spacetime-integral first variation, stationarity equivalence with all original metric equations and the complete weak original-field adjoint equations, and both recovery directions. Every stationary extended configuration projects to an original solution, and every original solution has a stationary zero-auxiliary lift. The proof also derives contracted Bianchi from actual metric and connection derivatives, weighted source conservation, and the gradient constraint at zero coupling. A combined terminal theorem includes the original metric equations and actual source conservation. Formal scope: smooth component fields on the full real four-coordinate domain, compatible metric and inverse fields, a smooth constitutive map, and compact auxiliary fields. No periodic boundary is imposed. The weak adjoint system is fully specified and proved; a separately rearranged strong covariant adjoint, arbitrary-open-domain localization, global manifold patching, action coordinate covariance as a Lean terminal, and unspecified microscopic matter equations are not claimed. Added adjoint fields mean that equal physical degrees of freedom and uniqueness of lifts are not established. This record contains the paper PDF, LaTeX source, Lean source dependencies, reproducible build instructions and independent fresh-source audit reports. The construction is an application of the established adjoint-field variational embedding, not a claim of a new universal principle. AI assistance was used for Lean code development and verification, translation, and accelerated multiplier searches and tests.