hilbert_variation_flat
plain-language theorem explainer
The result establishes that the Hilbert variation of the Einstein-Hilbert action vanishes identically in flat Minkowski spacetime when the metric and connection perturbations are set to zero. Gravitational physicists deriving the vacuum Einstein equations from the action principle cite this case as the base solution. The proof consists of a single application of the Minkowski vacuum solution lemma.
Claim. In Minkowski spacetime with metric $eta_{mu nu}$ and inverse $eta^{mu nu}$, the Hilbert variation of the Einstein-Hilbert action is satisfied for vanishing metric perturbation and vanishing connection perturbation.
background
The module defines the Einstein-Hilbert action as $S_{EH}[g] = (1/(2 kappa)) int R sqrt(-g) d^4 x$ and shows that its metric variation equals minus (1/(2 kappa)) times the Einstein tensor times the volume element. Setting the variation to zero recovers the vacuum Einstein field equations. This establishes Axiom 2 for the gravitational sector in the Recognition Science framework. The flat affine connection relies on the Kronecker delta defined in the Ndim connections module and the scalar coefficient mu from the projector module. The identity event from the observer forcing module supplies the zero-cost reference.
proof idea
The proof is a one-line wrapper that applies the Minkowski vacuum solution lemma to the given flat metric and zero variations.
why it matters
This theorem provides the flat spacetime verification required by the Hilbert variation certificate theorem, which also incorporates the Einstein tensor symmetry and flatness results. It completes the base case for Axiom 2 in the Einstein-Hilbert action derivation. In the Recognition Science framework, it connects the variational principle to the forcing chain steps that force three spatial dimensions and the recognition composition law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.