While this submission is a draft, it cannot be used by other submissions.

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.

Read the Lean proof on GitHub

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.