vertex_angular_deficit

formal source

 109
 110/-- Angular deficit at each vertex of Q₃: 2π − 3(π/2).
 111    Discrete curvature concentrated at the vertex. -/
 112noncomputable def vertex_angular_deficit : ℝ :=
 113  2 * Real.pi - faces_per_vertex * cube_dihedral
 114
 115theorem vertex_deficit_eq : vertex_angular_deficit = Real.pi / 2 := by
 116  unfold vertex_angular_deficit faces_per_vertex cube_dihedral; ring
 117
 118/-- **Discrete Gauss-Bonnet on Q₃**: total curvature of ∂Q₃
 119    (sum of vertex deficits over all 8 vertices) equals 4π.
 120
 121    8 × (π/2) = 4π = 2π · χ(S²). -/
 122theorem gauss_bonnet_Q3 :
 123    (cube_vertices D : ℝ) * vertex_angular_deficit = 4 * Real.pi := by
 124  have h8 : (cube_vertices D : ℝ) = 8 := by exact_mod_cast vertices_at_D3
 125  rw [h8, vertex_deficit_eq]; ring
 126
 127/-- Total solid angle of ∂Q₃ from any interior point, equal to
 128    the Gauss-Bonnet total curvature because ∂Q₃ ≅ S². -/
 129noncomputable def solid_angle_Q3 : ℝ :=
 130  (cube_vertices D : ℝ) * vertex_angular_deficit
 131
 132theorem solid_angle_Q3_eq : solid_angle_Q3 = 4 * Real.pi := gauss_bonnet_Q3
 133
 134/-- Per-face solid angle: by cubic symmetry, each of the 6 faces
 135    subtends equal solid angle 4π/6 = 2π/3 from the cube center. -/
 136noncomputable def per_face_solid_angle : ℝ :=
 137  solid_angle_Q3 / (cube_faces D : ℝ)
 138
 139theorem per_face_solid_angle_eq :
 140    per_face_solid_angle = 2 * Real.pi / 3 := by
 141  have h6 : (cube_faces D : ℝ) = 6 := by exact_mod_cast faces_at_D3
 142  simp only [per_face_solid_angle, solid_angle_Q3_eq, h6]; ring