Documentation

CslibFrontier.Computability.Complexity.Problems.Graph.PolygonalDrawing.Star

Genuine polygonal embeddings of stars of arbitrary degree #

The center is at zero and leaf i is at (i+1,1). Every edge is its actual straight segment. The segment-intersection proof has no degree restriction and includes the nullary star. This module proves embedding; clockwise realization is a separate order statement.

Main results #

source
def Cslib.Complexity.Graph.PolygonalDrawing.starPoint (n v : ℕ) :
ℂ

The center at zero, and the i-th leaf at (i+1,1).

Instances For
    source
    def Cslib.Complexity.Graph.PolygonalDrawing.star (n : ℕ) :
    (RotationSystem.starGraph n).PolygonalDrawing

    The explicit straight-segment drawing of the existing indexed star of any arity.

    Instances For
      source
      theorem Cslib.Complexity.Graph.PolygonalDrawing.star_isEmbedding (n : ℕ) :
      (star n).IsEmbedding

      The actual straight-segment star drawing is an embedding for every finite arity. Distinct edges meet only at their center, including when the degree is greater than four.