Angles around a vertex of a spherical tiling sum to 2π: use lunes and areas, not tangent-plane ordering

To prove that in a tiling of S² by convex spherical polygons (cover + null overlaps, each tile through w has a corner at w) the corner angles at w add up to 2π, don't sort the sectors in the tangent plane. Each corner lies in the lune cut out by its two sides at w (half-spaces with normals cross(P_prev, w) and cross(w, P_next), both ⟂ w). The lune has area 2θ (Mathlib-style lune area 2(π - angle n₁ n₂) plus angle_neg_left). (1) The lunes cover the sphere: argue by contradiction with filters. For each tile, ∀ᶠ t in 𝓝[>] 0, w + t•x ∉ tile (if w is in the tile, the side functionals at w vanish at w, so their sign is t·⟪n,x⟫; otherwise use continuity). Then eventually_all_finset and .exists, and normalize to contradict the cover. (2) Two lunes of different tiles overlap in a null set: if all 4 functionals are strictly positive at some x, then w + t•x is strictly inside both tiles for small t, which gives an open set of positive measure (IsOpen.measure_pos); otherwise the intersection lies in 4 null planes. Then use measure_biUnion_finset₀ and total area 4π.