hilbert_variation_cert
plain-language theorem explainer
hilbert_variation_cert assembles a certificate that the Einstein-Hilbert action variation produces the Einstein tensor and satisfies the vacuum field equations in flat spacetime. Researchers deriving general relativity from variational principles cite it to confirm G_mu nu = 0 follows from delta S_EH = 0. The proof is a direct term-mode record construction that wires in the flat Lagrangian vanishing, the flat variation theorem, and the symmetry plus vanishing properties of the Einstein tensor.
Claim. The Hilbert variation certificate holds in Minkowski spacetime: the Einstein-Hilbert Lagrangian density vanishes for nonzero kappa when the scalar curvature is zero; the Einstein tensor is symmetric whenever the Ricci tensor is symmetric; and the Einstein tensor itself vanishes identically.
background
The module defines the Einstein-Hilbert action as S_EH[g] = (1/(2 kappa)) integral R sqrt(-g) d^4 x and proves that its metric variation yields the Einstein tensor, thereby establishing Axiom 2. HilbertVariationCert is the structure that packages the necessary properties: flat_ok requires the variation to hold on Minkowski space with zero connection, eh_flat requires the Lagrangian density to vanish when curvature is zero, einstein_symmetric requires symmetry of the Einstein tensor when the Ricci tensor is symmetric, and einstein_flat requires the Einstein tensor to vanish on flat space.
proof idea
The proof is a term-mode record constructor for HilbertVariationCert. It supplies flat_ok by direct reference to hilbert_variation_flat, eh_flat by reference to the eh_flat theorem, einstein_symmetric by reference to RicciTensor.einstein_symmetric, and einstein_flat by reference to RicciTensor.einstein_flat.
why it matters
This declaration completes the proof of Axiom 2 (Hilbert variation) inside the gravity module, confirming that the Einstein-Hilbert action reproduces the vacuum Einstein equations without extra hypotheses in the flat limit. It sits downstream of the Ricci tensor definitions and upstream of any further gravitational dynamics in the Recognition framework. The result is consistent with the framework's derivation of three spatial dimensions and the Einstein tensor as the natural output of the action principle.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.