vacuum_efe_coord
plain-language theorem explainer
Defines the vacuum Einstein field equation in local coordinates as the condition that the Einstein tensor plus Lambda times the metric vanishes identically. Researchers deriving vacuum solutions or verifying the Hilbert variational principle cite this coordinate statement. The definition is a direct expansion of the Einstein tensor expression into component form.
Claim. The vacuum Einstein field equation states that for all indices $mu, nu$, $G_{mu nu} + Lambda g_{mu nu} = 0$, where $G_{mu nu}$ is the Einstein tensor constructed from the metric $g$, its inverse, the connection coefficients, and their first derivatives.
background
In the Gravity.RicciTensor module the Einstein tensor is obtained from the Ricci tensor via $G_{mu nu} = R_{mu nu} - (1/2) R g_{mu nu}$, with the Ricci tensor itself the contraction $R_{mu nu} = R^rho_{mu rho nu}$ of the Riemann tensor. The metric is supplied by the structure MetricTensor whose field g : Idx → Idx → ℝ is required to be symmetric; InverseMetric supplies the inverse components satisfying the usual contraction identity. Idx is the abbreviation Fin 4. These structures are imported from Gravity.Connection and rest on the local non-sealed metric interface in Foundation.Hamiltonian.
proof idea
This is a definition, not a theorem. It directly encodes the coordinate form of the vacuum Einstein equation by substituting the definition of einstein_tensor into the displayed forall statement.
why it matters
The definition is invoked by hilbert_variation_holds to express the variational principle for the Einstein-Hilbert action, by minkowski_is_vacuum_solution to certify that flat spacetime satisfies the vacuum equation with Lambda = 0, and by RicciCert and the stress-energy certificates that treat vacuum as the T = 0 special case. It supplies the coordinate anchor for the Einstein tensor symmetry and flatness results inside the RicciTensor module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.