An Extended Action for Gravitational Aether with Exact Recovery of the Classical Solution Set

We give a local covariant extended action for the classical gravitational-aether equations. Independent multiplier fields are paired with the metric equation, matter conservation, aether evolution and four-velocity normalization. Successive integration with respect to these fields determines the action, and a two-direction argument proves that its stationary configurations project exactly onto all solutions of the original equations. No irrotational-flow restriction, cosmological symmetry reduction or periodic boundary condition is imposed. A scalar-matter calculation identifies a failure of direct metric pairing and illustrates why a multiplier that repairs one sector need not repair the full system. The construction applies the established formal-Lagrangian method; it does not establish equality of physical degrees of freedom or provide a quantum completion. Accompanying Lean code verifies the continuous-integral projection theorem with explicit component equations and stated regularity assumptions. This deposit contains the manuscript PDF and the LaTeX source with the Lean proof package, reproduction script, theorem-to-text mapping, source hashes, and actual build and axiom-audit logs. A clean build on October 27, 2026 passed all seven targets and audited 61 public theorems. Section 6 of the manuscript and the ancillary README specify the assumptions and scope of formal verification. Version 1.1 — core verification supplement, 28 October 2026. A fresh verification passed 19/19 build targets and audited 91 public theorems. The verified result concerns the complete four-dimensional incompressible macroscopic coordinate equations with supplied matter stress and the stated compatible parameter curves. It includes the actual integral variation and exact projection of the extended stationary set onto the original solution set, under the hypotheses recorded in SCOPE and the theorem map. No microscopic matter theory or global manifold construction is claimed. This supplement does not certify every supplementary discussion or search classification in the original paper, establish physical degrees-of-freedom equivalence, or assert bibliographic priority. Use Gravitational_Aether_Core_Verification_Scope_20261028.pdf and Gravitational_Aether_Core_Lean_Verification_20261028.zip for the current formal scope. The original manuscript and earlier proof package are retained unchanged; the seven-target/61-theorem counts above describe that historical package. AI tools were used to assist Lean code development and verification, translation, and to accelerate multiplier searches and tests.