65theorem flat_deficit_zero : deficit_angle_flat = 0 := by
proof body
Term-mode proof.
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. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.