An Extended Variational Formulation of Schouten-Codazzi Field Equations

We construct a covariant extended action for the Schouten-Codazzi field equations using independent adjoint tensor fields. Variation of these fields recovers the original Schouten-source equation and the complete Codazzi condition. Every original solution has a stationary lift with vanishing adjoint fields, and every stationary configuration projects to an original solution. Original algebraic admissibility prescriptions are retained. Version 1.1 expands the Lean formalization from the earlier chart-level core to the actual geometric equations, their coordinate covariance, a single globally defined action, its complete first variation at general nonzero adjoint fields, and equality of the projected stationary and original solution sets. The archive contains the manuscript, proof sources, a theorem-to-manuscript map, reproducible verification scripts, build logs, and source checksums. The verification report states the hypotheses and the exact scope of each result. This is an extended variational formulation using the established formal-Lagrangian construction; it does not claim an auxiliary-free action, equality of physical degrees of freedom, or a new general variational theorem. AI tools were used to assist Lean code development and verification, translation, and to accelerate multiplier searches and tests.