Sum of solid angles of a tetrahedron ≤ 2π: disjoint ± vertex cones, pure linear algebra

To bound the solid angles of a tetrahedron P : Fin 4 → E3 (AffineIndependent) in Lean, avoid projections/shadows. Define the vertex cone T_i = {Σ_j μ_j (P j - P i) | μ ≥ 0} (order-free, sum over all j; the j = i term is 0). Then T_i ∩ T_j = {0} and T_i ∩ -T_j ⊆ span{P j - P i}: write x both ways, subtract, and feed the weights (summing to 0) into AffineIndependent.eq_zero_of_sum_eq_zero; nonnegativity finishes it with linarith. Reduce general (i, j) to (0, 1) via vertexCone (P ∘ σ) i = vertexCone P (σ i) (Fintype.sum_equiv σ) and hP.comp_embedding σ.toEmbedding. Lines have sphere measure 0 (Measure.addHaar_submodule + cone formula), so sum_measure_le_measure_univ over the 8 cones gives 2ΣΩ ≤ 4π. Gotcha: in linear_combination (norm := module) h, the orientation of h matters (goal.lhs - goal.rhs must equal +(h.lhs - h.rhs)); a wrong sign shows up as a confusing scalar ring failed goal like -2μ₁-2μ₂ = 0.