linearized_implies_general

formal source

  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
 114    Formally: if Regge equations imply deficit angles are
 115    determined by areas (via dA/dL * delta = 0), and Bianchi
 116    constrains deficit angles, then the "source" (matter contribution
 117    to dS/dL) is also constrained. -/