Face angles at a polyhedron vertex < 2π without a cyclic order: count crossing planes on the sphere
To prove Euclid XI.21 (angular defect > 0) when your polyhedron data does not record the cyclic order of faces around a vertex, don't build the vertex figure. For each face sector with edges a, b (angle θ), the unit normals y whose plane y⊥ separates a from b form two antipodal lunes of area 4θ (lune formula for half-spaces a and -b, plus -a and b; the boundary planes are null). A plane through the apex crosses at most two sectors. Take r_p = |⟪b,y⟫|a + |⟪a,y⟫|b in y⊥. Three such rays satisfy c1 r1 + c2 r2 + c3 r3 = 0 with c_i = ⟪y, r_j × r_k⟫. Each face normal N_i kills r_i and is strictly negative on the other two rays, which forces c3 = 0, so r1 ∥ r2, which is a contradiction. No plane crosses near an inward direction, an open set of positive measure (IsOpenPosMeasure on Measure.toSphere). Integrate the indicator sum (lintegral_finsetSum + lintegral_indicator_one): 4∑θ ≤ 2·σ(Gᶜ) < 8π.
Update: the cyclic order can in fact be recovered from the same data. Define succ p = corner at v of the face across the side leaving p; it is injective because a side appears reversed in the neighbouring face. That it is a single cycle follows by contradiction: with two cycles, tilt the plane spanned by one edge from each cycle so that both cycles have edges on both sides, and the parity count gives 4 crossed faces, against the at-most-2 bound used here. No three edges at a vertex are coplanar, via the supporting functionals C f + C g. This also gives Gram's relation for general convex polyhedra by the same Crofton counting on the normal cone.