vacuum_efe_coord
The declaration defines the vacuum Einstein field equation in local coordinates as the condition that the Einstein tensor plus Lambda times the metric vanishes for all index pairs. Researchers deriving vacuum solutions or verifying the Hilbert variational principle in Recognition Science gravity would cite this predicate. It is introduced as a direct definition that expands the Einstein tensor expression without invoking additional lemmas.
claimThe vacuum Einstein field equation in coordinates asserts that $G_{mu nu} + Lambda g_{mu nu} = 0$ for all indices $mu, nu$, where $G_{mu nu}$ is the Einstein tensor built from the metric components $g$, its inverse, the Christoffel symbols gamma, and their first derivatives dgamma.
background
The RicciTensor module constructs the Ricci tensor by contraction of the Riemann tensor, the scalar curvature by further contraction with the inverse metric, and the Einstein tensor as $G_{mu nu} = R_{mu nu} - (1/2) R g_{mu nu}$. The MetricTensor structure supplies a symmetric bilinear form $g : Idx -> Idx -> R$ on Idx = Fin 4, while InverseMetric supplies the corresponding inverse components satisfying the delta identity. Upstream results from the Connection module establish these metric structures; the Euler-Mascheroni constant appears only in unrelated constant definitions.
proof idea
This is a definition that directly states the coordinate form of the vacuum Einstein equation by requiring the Einstein tensor plus Lambda times the metric to vanish identically. It relies on the prior definition of einstein_tensor in the same module and performs no further reduction.
why it matters in Recognition Science
This predicate serves as the target for the Hilbert variational principle in the EinsteinHilbertAction module, where hilbert_variation_holds reduces to vacuum_efe_coord with Lambda set to zero. It also underpins the proof that Minkowski space is a vacuum solution and the RicciCert structure. In the Recognition framework it encodes the vacuum case of the Einstein field equations, consistent with the divergence-free property of the Einstein tensor established earlier in the module.
scope and limits
- Does not assert existence of non-trivial solutions.
- Does not incorporate matter sources or stress-energy.
- Does not derive the equation from a variational principle.
- Does not specify dimension or signature beyond the Idx = Fin 4 interface.
Lean usage
theorem minkowski_is_vacuum_solution : vacuum_efe_coord minkowski minkowski_inverse (fun _ _ _ => 0) (fun _ _ _ _ => 0) 0 := by intro mu nu; simp [einstein_flat]formal statement (Lean)
97def vacuum_efe_coord (met : MetricTensor) (ginv : InverseMetric)
98 (gamma : Idx → Idx → Idx → ℝ)
99 (dgamma : Idx → Idx → Idx → Idx → ℝ)
100 (Lambda : ℝ) : Prop :=
proof body
Definition body.
101 ∀ mu nu : Idx,
102 einstein_tensor met ginv gamma dgamma mu nu + Lambda * met.g mu nu = 0
103
104/-- The sourced Einstein field equation:
105 G_{mu nu} + Lambda g_{mu nu} = kappa T_{mu nu} -/