flat_deficit_zero

formal source

  62    4 cubes × (pi/2 dihedral) = 2*pi = full rotation = no deficit. -/
  63noncomputable def deficit_angle_flat : ℝ := 2 * Real.pi - cubes_per_edge * cube_dihedral
  64
  65theorem flat_deficit_zero : deficit_angle_flat = 0 := by
  66  unfold deficit_angle_flat cubes_per_edge cube_dihedral
  67  simp; ring
  68
  69/-- The deficit angle at an edge of a DEFORMED lattice.
  70    When the metric perturbation h deforms the cube, each dihedral angle
  71    changes by delta_theta ≈ (a^2/4) * (second derivative of h).
  72
  73    The deficit angle is: delta = -sum of dihedral changes
  74    = -4 * delta_theta = -a^2 * (d^2 h / dx^2) in the leading order. -/
  75noncomputable def deficit_angle_deformed (d2h : ℝ) (a : ℝ) : ℝ := -a ^ 2 * d2h
  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