An Extended Action for the Lattice Schwarzian Boussinesq Equation with Exact Recovery of the Solution Set

We give a local auxiliary-field action for the complete nine-point lattice Schwarzian Boussinesq equation, retaining its original rational expression and nonzero-denominator domain. The stationary configurations project exactly onto the full original solution set, for arbitrary finite collections of overlapping cells and for the whole integer lattice with finitely supported auxiliary fields and variations. No periodic boundary condition or decay of the original field is imposed. Version 1.1 expands the Lean formalization to the explicit real and complex equations, actual first and second variations, full nodal adjoint equations, preservation of the original domain, exact recovery, counterexamples, the centered point-multiplier obstruction, and the specified bounded multiplier searches. The search proofs connect actual derivatives of the original equation to admissible exact samples, denominator clearing and kernel-checked rank certificates. The manuscript and theorem map retain the parameter values and search scopes of each result. The archive includes the PDF, LaTeX sources, complete proof sources, reproducible verification scripts, build logs and checksums. This is an explicit application of the established discrete formal-Lagrangian method. It does not provide the missing single-original-field Lagrangian or a Lagrangian multiform, and it does not claim equality of physical degrees of freedom or an unrestricted impossibility theorem. AI tools were used to assist Lean code development and verification, translation, and to accelerate multiplier searches and tests.