solid_angle_Q3_eq

formal source

 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
 143
 144/-- Face solid angles reconstruct the total: 6 × (2π/3) = 4π. -/
 145theorem face_solid_angle_sum :
 146    (cube_faces D : ℝ) * per_face_solid_angle = 4 * Real.pi := by
 147  have h6 : (cube_faces D : ℝ) = 6 := by exact_mod_cast faces_at_D3
 148  rw [per_face_solid_angle_eq, h6]; ring
 149
 150/-! ## Part 4: Geometric Seed Assembly -/
 151
 152/-- The geometric seed factor is the passive edge count.
 153    This is WHERE THE 11 COMES FROM. -/
 154def geometric_seed_factor : ℕ := passive_field_edges D
 155
 156/-- Verify: geometric_seed_factor = 11 -/
 157theorem geometric_seed_factor_eq_11 : geometric_seed_factor = 11 := by native_decide
 158
 159/-- The full geometric seed: Ω(∂Q₃) × E_passive.
 160    Both factors derive from Q₃ geometry:
 161    - 4π = Gauss-Bonnet total curvature of ∂Q₃ (Part 3)
 162    - 11 = cube edges − 1 active edge (Part 2) -/