HilbertVariationCert
plain-language theorem explainer
The certificate structure packages the flat-space checks and symmetry properties needed to confirm that the Einstein-Hilbert action varies to the Einstein tensor. Researchers working on variational derivations of general relativity cite this when confirming vacuum solutions. The definition simply assembles four already-proved facts: the action density vanishes when curvature is zero, the Einstein tensor is symmetric, and it vanishes on Minkowski space.
Claim. A certificate asserting that the Einstein-Hilbert Lagrangian density vanishes in flat spacetime ($L_{EH}(0,det g, kappa)=0$ for $kappa neq 0$), that the Einstein tensor $G_{mu nu}$ is symmetric in its indices, and that $G_{mu nu}(eta, eta^{-1}, 0, 0)=0$ for the Minkowski metric with zero connection derivatives.
background
The Einstein-Hilbert action is defined as $S_{EH}[g] = (1/(2 kappa)) integral R sqrt(-g) d^4 x$. Its variation with respect to the inverse metric produces the Einstein tensor $G_{mu nu} = R_{mu nu} - (1/2) R g_{mu nu}$. The module proves this yields the vacuum field equations $G_{mu nu}=0$ once the action is stationary. Key objects include the Minkowski metric eta = diag(-1,1,1,1) from Connection.minkowski, its inverse, the Lagrangian density $L = R sqrt(|det g|)/(2 kappa)$ from eh_lagrangian_density, and the Einstein tensor built from the Ricci tensor. Upstream, eh_flat shows $L=0$ when $R=0$, while RicciTensor supplies the symmetry and flat vanishing lemmas. This setting assumes the connection infrastructure but defers full covariant derivatives.
proof idea
The structure is defined by direct field assignment. flat_ok pulls from hilbert_variation_flat, eh_flat from the eh_flat theorem, einstein_symmetric from RicciTensor.einstein_symmetric, and einstein_flat from RicciTensor.einstein_flat. No tactics are needed beyond the structure constructor.
why it matters
hilbert_variation_cert instantiates this certificate to prove Axiom 2 of the Recognition framework: the Hilbert variational principle. The result derives the vacuum Einstein equations from the action without assuming them. It sits after the Ricci tensor definitions and before any matter coupling or cosmological term extensions. The open question remains the full Palatini identity for non-flat connections.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.