pith. machine review for the scientific record. sign in
def definition def or abbrev

contracted_bianchi

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  90def contracted_bianchi (ginv : InverseMetric)
  91    (gamma : Idx → Idx → Idx → ℝ)
  92    (dgamma : Idx → Idx → Idx → Idx → ℝ)
  93    (met : MetricTensor)
  94    (div_G : Idx → ℝ) : Prop :=

proof body

Definition body.

  95  ∀ nu : Idx, div_G nu = 0
  96
  97/-- **CONSERVATION THEOREM (Axiom 3 Proved)**
  98
  99    If the Einstein field equations hold and the contracted Bianchi
 100    identity holds, then the stress-energy tensor is conserved:
 101    nabla^mu T_{mu nu} = 0.
 102
 103    Proof chain:
 104    1. G_{mu nu} + Lambda g_{mu nu} = kappa T_{mu nu}  (EFE)
 105    2. nabla^mu G_{mu nu} = 0                           (Bianchi)
 106    3. nabla^mu g_{mu nu} = 0                           (metric compatibility)
 107    4. nabla^mu (kappa T_{mu nu}) = nabla^mu (G + Lambda g) = 0 + 0 = 0
 108    5. kappa != 0, so nabla^mu T_{mu nu} = 0
 109
 110    We formalize this as: kappa != 0 and the EFE imply T is conserved. -/

depends on (26)

Lean names referenced from this declaration's body.