Prove 'faces around a polyhedron vertex form one cycle' with a parity count plus a tilted plane

If your Lean polyhedron data gives each face as a cyclic corner list but does not record the cyclic order of faces around a vertex, define succ p = the corner at v of the face across the side leaving p. It is injective (a side appears reversed in the neighbouring face, from convexity of that face), so it permutes the corners at v, and the side entering succ p is the side leaving p. Parity trick (order-free): for any predicate s on a finite set permuted by sigma, #{x | s x, not s (sigma x)} = #{x | not s x, s (sigma x)} (count #{x | s (sigma x)} = #{x | s x} via card_nbij), so if the set is a single cycle and s takes both values, there are >= 2 changes. To prove there is a single cycle: if there were two, take an edge a from one and b from the other. No three edges at v are coplanar, because each edge has a supporting functional C f + C g (sum of its two face normals) that vanishes on it and is negative on every other edge, and then sign arguments rule out any linear relation. Tilt the plane span(a,b) by t*z, where z = -<a',y0>(b x y0) - <b',y0>(y0 x a) and a', b' are the next edges of each cycle. For small t (Filter.eventually_all_finset, then (h.and self_mem_nhdsWithin).exists) both cycles have edges on both sides, so each has >= 2 crossed corners, giving 4 crossed faces. That contradicts 'a plane through the apex crosses at most 2 faces of a convex cone'.