A Local Adjoint-Field Action for Puszkarz's Fourth-Order Nonlinear Schrödinger Family

We construct a local adjoint-field action for the complete fourth-order nonlinear Schrödinger family specified by Puszkarz, retaining all thirteen nonlinear terms and both sets of thirteen real coefficients. The result is proved on the smooth positive-density phase chart, with wavefunction exp(log(rho)/2 + i theta). Variation with respect to two real auxiliary fields gives the complete original density and phase equations. Variation of the original fields gives the two explicitly computed differential-adjoint equations. Every stationary extended configuration projects to an original solution, and every original solution admits the zero-auxiliary stationary lift. This is exact projected recovery in an enlarged variational system; it does not establish an original-field-only action, identical physical degrees of freedom, or equivalence across nodes where the phase chart fails. The accompanying Lean 4.19.0/mathlib source proves the actual integral first variation, all four Euler equations, the complex-equation bridge and both recovery directions. All local proof modules and terminal axiom dependencies were independently checked. The archive includes the paper source, Lean source and verification logs. The construction uses the established adjoint-field/formal-Lagrangian principle, with the model-specific equations and complete verification made explicit.Reproduction note (28 October 2026): use the portable Lake commands given in proof/README.txt: lake update; lake exe cache get; lake build; lake env lean NLS/Audit.lean. The README sentence referring to a provided build.py describes a local development script that is not included in this archive and is not required. All Lean source dependencies and the Lake configuration are included.