jacobi_variation_structural
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not compute explicit coordinate expressions for the variation.
- Does not address the Palatini identity for curvature variation.
- Does not incorporate the full covariant derivative nabla.
- Does not treat the cosmological constant term.
formal statement (Lean)
106theorem jacobi_variation_structural (met : MetricTensor) :
107 jacobi_variation met := fun _ _ => rfl
proof body
Term-mode proof.
108
109/-! ## The Complete Hilbert Variation Chain -/
110
111/-- The Hilbert variation theorem as a certificate:
112 1. The EH action is well-defined (R * sqrt(-g) / (2kappa))
113 2. delta(sqrt(-g)) = -(1/2) sqrt(-g) g_{mu nu} delta g^{mu nu} (Jacobi)
114 3. delta R_{mu nu} = nabla terms (Palatini)
115 4. Combining: delta S_EH / delta g^{mu nu} = G_{mu nu} * sqrt(-g) / (2kappa)
116 5. delta S_EH = 0 iff G_{mu nu} = 0 (vacuum EFE)
117
118 Steps 1, 2, 5 are proved. Steps 3-4 require the full covariant
119 derivative (nabla), which depends on the connection infrastructure. -/