linearized_bianchi

formal source

  80
  81/-- In the linearized regime (small deficit angles), the Bianchi
  82    identity reduces to: sum of deficit angles = 0 exactly. -/
  83def linearized_bianchi (deficit_angles : List ℝ) : Prop :=
  84  deficit_angles.sum = 0
  85
  86/-- The linearized Bianchi identity implies the general one (with n = 0). -/
  87theorem linearized_implies_general (deficits : List ℝ)
  88    (h : linearized_bianchi deficits) :
  89    discrete_bianchi_identity deficits :=
  90  ⟨0, by unfold linearized_bianchi at h; simp [h]⟩
  91
  92/-- For a flat lattice, all deficits are zero, so Bianchi is trivially satisfied. -/
  93theorem flat_bianchi (deficits : List ℝ) (h : ∀ d ∈ deficits, d = 0) :
  94    linearized_bianchi deficits := by
  95  unfold linearized_bianchi
  96  induction deficits with
  97  | nil => simp
  98  | cons a as ih =>
  99    simp only [List.sum_cons]
 100    have ha : a = 0 := h a (List.mem_cons_self ..)
 101    rw [ha, zero_add]
 102    exact ih (fun d hd => h d (List.mem_cons_of_mem _ hd))
 103
 104/-! ## Conservation from Bianchi -/
 105
 106/-- The discrete conservation law: if the Regge equations hold
 107    (delta S / delta L_e = 0 for all edges e) and the discrete
 108    Bianchi identity holds, then the discrete stress-energy is
 109    conserved.
 110
 111    This mirrors the continuum: nabla^mu G_mu_nu = 0 (Bianchi)
 112    + G_mu_nu = kappa T_mu_nu (Einstein) => nabla^mu T_mu_nu = 0.
 113