hilbert_variation_closure
plain-language theorem explainer
The Hilbert variation of the Einstein-Hilbert action is packaged as a closed certificate for the FullEFE module: flat-space checks, Einstein-tensor symmetry, and vanishing on flat metrics all hold. Anyone assembling the RS full-GR or derivation-chain certificates cites this. Proof is a one-line re-export of the EinsteinHilbertAction certificate.
Claim. The Hilbert-variation closure holds: the Einstein-Hilbert action variation certificate is available in the FullEFE setting, recording that the flat-space Hilbert variation is valid, the Einstein-Hilbert density is correct on flat metrics, and the Einstein tensor is symmetric and vanishes on flat backgrounds.
background
Module FullEFE derives the complete nonlinear, sourced Einstein field equations from the RS discrete ledger, conditional on Regge convergence axioms. The derivation chain runs from J-cost minimization on the ledger, through the Regge action and its continuum limit, to variational convergence of the Einstein-Hilbert action.
Step 5 of that chain is classical: stationary variation of the Einstein-Hilbert action yields the vacuum Einstein equations. The certificate type (aliased here as Hilbert-variation closure) bundles the supporting facts already proved in EinsteinHilbertAction and RicciTensor: the flat-space Hilbert variation, the Einstein-Hilbert density on flat metrics, symmetry of the Einstein tensor, and its vanishing on flat backgrounds.
Upstream, hilbert_variation_cert assembles exactly those four fields into one record. This declaration simply exposes that record under the FullEFE naming so later certificates can cite a single local name.
proof idea
One-line wrapper. The proof is the term EinsteinHilbertAction.hilbert_variation_cert, which already constructs a HilbertVariationCert from four lemmas: flat-space Hilbert variation, flat Einstein-Hilbert density, Einstein-tensor symmetry, and Einstein-tensor vanishing on flat metrics. No extra tactics or algebraic work occur here; the abbrev HilbertVariationClosure is definitionally that same certificate type.
why it matters
Closes step 5 of the FullEFE chain (vacuum EFE from Hilbert variation) with a theorem-backed certificate rather than a placeholder Prop. Downstream, full_gr_certificate_v2 takes this as its hilbert_variation field alongside matter coupling; rs_derivation_chain and full_gr_certificate sit in the same assembly path for the RS-specific full GR package.
In the broader RS gravity story this is the continuum variational link between the Regge/ledger side and classical GR: once Regge action converges to Einstein-Hilbert and variations pass to the limit, this certificate says the vacuum equations are the critical-point condition. Kappa derivation ($\kappa = 8\varphi^5$), Bianchi conservation, and matter coupling are separate siblings; nonlinear Regge convergence remains the main external axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.