HilbertVariationClosure
plain-language theorem explainer
Aliases the Hilbert-variation certificate into the full-EFE module: vacuum stationarity of the Einstein–Hilbert action is equivalent to vanishing Einstein tensor. Gravity and continuum-limit authors cite it as step 5 of the RS→EFE chain. The body is a pure type synonym; no new proof work lives here.
Claim. Write $H$ for the certificate that the Einstein–Hilbert action $S_{\mathrm{EH}}=\int R\sqrt{-g}/(2\kappa)$ is well-defined, that the Jacobi and Palatini identities hold for $\delta\sqrt{-g}$ and $\delta R_{\mu\nu}$, and that $\delta S_{\mathrm{EH}}=0$ if and only if $G_{\mu\nu}=0$ in vacuum. The present name is simply that same certificate, re-exported for the full-EFE derivation chain.
background
The FullEFE module assembles the complete nonlinear, sourced Einstein field equations from the Recognition Science discrete ledger, conditional on Regge-convergence axioms. The documented chain runs: J-cost minimization on the ledger → Regge action → continuum Einstein–Hilbert limit → variational convergence → Hilbert variation (vacuum EFE) → matter coupling → Bianchi conservation, with $\kappa=8\varphi^5$ derived rather than fitted.
Upstream, the Einstein–Hilbert action module packages the classical Hilbert variation as a certificate structure. Its doc-comment states the five ingredients: the EH density $R\sqrt{-g}/(2\kappa)$; Jacobi’s formula $\delta\sqrt{-g}=-(1/2)\sqrt{-g},g_{\mu\nu}\delta g^{\mu\nu}$; Palatini’s identity that $\delta R_{\mu\nu}$ is a pure divergence; the combination yielding $\delta S_{\mathrm{EH}}/\delta g^{\mu\nu}=G_{\mu\nu}\sqrt{-g}/(2\kappa)$; and the vacuum equivalence $\delta S_{\mathrm{EH}}=0\Leftrightarrow G_{\mu\nu}=0$. Steps 1, 2, and 5 are proved there; 3–4 still need the full covariant calculus.
This abbreviation does not restate those identities. It only re-exports the certificate type so the full-EFE structures can name step 5 without importing the action module’s internal names.
proof idea
There is no proof body. The declaration is a one-line type synonym: the local name is definitionally equal to the upstream Hilbert-variation certificate structure. Downstream theorems that need an inhabitant simply apply the existing certificate constructor from the Einstein–Hilbert action module (the companion theorem hilbert_variation_closure does exactly that).
why it matters
In the module’s eight-step chain this is step 5: once Regge action has converged variationally to Einstein–Hilbert, vacuum stationarity must recover $G_{\mu\nu}=0$. The full derivation-chain structure records that step under this name; both GR certificate bundles (v1 and v2) require an inhabitant of it among their proved or certified fields.
Framework-wise it sits after the J-cost → Regge → continuum path (steps 1–4) and before matter coupling and Bianchi conservation (steps 6–7). Kappa derivation ($\kappa=8\varphi^5$) is independent and already proved. The remaining open gate is step 3: full nonlinear Regge→EH convergence remains axiomatized (the linearized second-order estimate is theorem-backed). Re-exporting the Hilbert certificate keeps the vacuum-EFE link cleanly separated from that external analytic hypothesis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.