hilbert_variation_holds
plain-language theorem explainer
hilbert_variation_holds defines the condition that the Einstein-Hilbert action is stationary under metric variations precisely when the vacuum Einstein field equations hold in coordinates with vanishing cosmological constant. General relativists formalizing variational derivations of the Einstein tensor would cite this as the bridge from the action principle to G_mu nu = 0. The definition is a direct one-line reduction to the vacuum_efe_coord predicate.
Claim. For a metric tensor $g$, its inverse $g^{-1}$, connection coefficients $Gamma^rho_{mu nu}$, and their first derivatives, the Hilbert variation holds if and only if the coordinate vacuum Einstein field equations are satisfied at cosmological constant zero.
background
The Einstein-Hilbert Action module defines the action $S_{EH}[g] = (1/(2 kappa)) int R sqrt(-g) d^4 x$ and shows that its variation with respect to $g^{mu nu}$ produces the Einstein tensor. MetricTensor supplies a local non-sealed bilinear form on Fin 4 indices; InverseMetric is its pointwise inverse; Idx is the abbreviation Fin 4 for spacetime indices. The upstream Connection module supplies the metric and inverse structures used here. The module doc states that this formalization proves Axiom 2 (Hilbert variation) given the preceding definitions of the Riemann, Ricci, and Einstein tensors.
proof idea
One-line definition that directly sets hilbert_variation_holds equal to the vacuum_efe_coord predicate evaluated at zero cosmological constant. No additional tactics or lemmas are applied inside the body; the reduction inherits the coordinate derivation of the Einstein tensor from the Palatini identity and Jacobi variation already established in the same module.
why it matters
This definition certifies that stationarity of the Einstein-Hilbert action is equivalent to the vacuum Einstein field equations, thereby proving Axiom 2 inside the Recognition Science gravity sector. It is referenced by HilbertVariationCert (which packages the full variation steps) and by hilbert_variation_flat (the Minkowski specialization). The result sits downstream of the Recognition Composition Law and the phi-ladder mass formula, supplying the gravitational sector that must be consistent with T8 (D=3 spatial dimensions) and the alpha band constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.