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 full nine-point lattice Schwarzian Boussinesq equation, retaining its original rational expression and nonzero-denominator domain. The stationary configurations project exactly onto all original solutions, both 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. The manuscript also derives a point-multiplier obstruction and reports exact, independently reconstructed certificates for several bounded multiplier searches. The construction is an explicit application of the established discrete formal-Lagrangian method of L. Peng. It does not provide the missing single-original-field Lagrangian or a Lagrangian multiform. The deposit includes the manuscript PDF, LaTeX sources, Lean proofs, build and axiom-audit logs, and exact symbolic computation scripts and certificates. The manuscript and accompanying theorem map state precisely which results are Lean-verified; the bounded search certificates are separately checked by exact computation.