Proof of `Stars are outerplanar`
groundedproofs/Lax303502Proofs/Stars.lean · lax-303502
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
Every finite star has a straight-line drawing with its vertices on a circle.
Proof strategy
Choose distinct real parameters for the vertices and use the rational parametrization of the unit circle. A tangent to the circle at any vertex strictly separates that vertex from every chord with different endpoints. All edges of the star contain its centre, so there are no vertex-disjoint edges whose segments could cross. The construction includes the one-vertex star.
Attribution
Direct elementary circle construction. Diestel, Graph Theory, sixth edition, Chapter 4, supplies the plane-drawing framework and the outerplanarity definition in Exercise 23, but does not give this explicit parametrization. The coordinate proof here is supplied in full and uses no planarity theorem.