jacobi_variation_structural
plain-language theorem explainer
The structural Jacobi variation asserts that the first-order change in the spacetime volume element for any metric tensor obeys the standard trace identity. Researchers deriving the Einstein field equations from the Hilbert action cite this identity when evaluating the functional derivative of the action. The proof is a one-line reflexivity wrapper that directly invokes the definition of the variation operator.
Claim. For any metric tensor $g$, the Jacobi variation holds: $delta(sqrt(-g)) = -frac12 sqrt(-g) g_{mu nu} delta g^{mu nu}$.
background
The Einstein-Hilbert action is the integral of the scalar curvature times the volume element $sqrt(-g)$, and the module proves that its metric variation yields the Einstein tensor, establishing the Hilbert variational principle as a theorem. The MetricTensor structure supplies a local non-sealed bilinear form on four-dimensional space. Upstream results include the Chain structure providing minimal axioms for standalone compilation and the Kronecker delta on Fin n used in projections and connections.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of jacobi_variation.
why it matters
This declaration supplies the structural Jacobi identity required for the Hilbert variation chain, feeding into hilbert_variation_holds and the full derivation of the vacuum Einstein equations. It corresponds to step 2 in the documented chain (delta sqrt(-g) identity) and supports the proved status of Axiom 2 in the module. In the Recognition Science framework it anchors the action principle consistent with the eight-tick octave and D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.