pith. machine review for the scientific record. sign in
theorem proved term proof

flat_deficit_zero

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 125theorem flat_deficit_zero (h : HingeData)
 126    (h_flat : h.dihedral_angles.sum = 2 * Real.pi) :
 127    deficit_angle h = 0 := by

proof body

Term-mode proof.

 128  unfold deficit_angle; linarith
 129
 130/-- On the flat cubic lattice Z^3, each edge is shared by 4 cubes.
 131    Each cube contributes dihedral angle pi/2.
 132    Sum = 4 * pi/2 = 2*pi, so deficit = 0. -/

used by (2)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.