deficit_zero_when_flat

formal source

  76
  77/-- The deficit angle vanishes when the second derivative of h is zero
  78    (flat metric perturbation = constant or linear h). -/
  79theorem deficit_zero_when_flat (a : ℝ) : deficit_angle_deformed 0 a = 0 := by
  80  unfold deficit_angle_deformed; ring
  81
  82/-- The deficit angle scales with the lattice spacing squared. -/
  83theorem deficit_scales_with_a_squared (d2h a1 a2 : ℝ) (ha : a2 = 2 * a1) :
  84    deficit_angle_deformed d2h a2 = 4 * deficit_angle_deformed d2h a1 := by
  85  unfold deficit_angle_deformed; rw [ha]; ring
  86
  87/-! ## Deficit Angle to Curvature -/
  88
  89/-- The curvature is the deficit angle divided by the dual area.
  90    For a cubic lattice with spacing a, the dual area of each edge is a^2.
  91    So curvature = deficit / a^2 = -d^2h/dx^2 (the second derivative!). -/
  92noncomputable def curvature_from_deficit (deficit_angle area : ℝ) : ℝ :=
  93  deficit_angle / area
  94
  95/-- The curvature from a deformed lattice equals minus the second derivative
  96    of the metric perturbation. This is the KEY BRIDGE:
  97    lattice deficit angle -> continuum curvature. -/
  98theorem curvature_equals_d2h (d2h a : ℝ) (ha : a ≠ 0) :
  99    curvature_from_deficit (deficit_angle_deformed d2h a) (a ^ 2) = -d2h := by
 100  unfold curvature_from_deficit deficit_angle_deformed
 101  have ha2 : a ^ 2 ≠ 0 := pow_ne_zero 2 ha
 102  field_simp [ha2]; ring
 103
 104/-- In linearized gravity, the Ricci scalar R is related to the second
 105    derivatives of h. For a trace-reversed perturbation in harmonic gauge:
 106    R = -nabla^2(trace h) + div div h
 107
 108    For a scalar perturbation h = Phi * delta_ij (Newtonian gauge):
 109    R = -2 * nabla^2 Phi