2.17. Polygonal Geometry Prerequisites🔗

Componentwise numerical genus zero is equivalent to an actual polygonal embedding realizing the supplied literal clockwise rotation, when all incident endpoints are declared. Both general directions are proved below. Topological taming, indexed FZ versus DK set conventions and source comparison, frozen-switch completeness, Hanani–Tutte recognition and the full #3091 endpoint remain open.

The ordinary imports at the start of this chapter include CslibFrontier.Computability.Complexity.Problems.Graph.PolygonalDrawing.Germs, CslibFrontier.Computability.Complexity.Problems.Graph.PolygonalDrawing.Neighborhood, CslibFrontier.Computability.Complexity.Problems.Graph.PolygonalDrawing.Points, CslibFrontier.Computability.Complexity.Problems.Graph.PolygonalDrawing.Star and CslibFrontier.Computability.Complexity.Problems.Graph.ClosedPassages.Loop. They expose the following clients without import all.

Cslib.Polygonal.Route lists bends + 2 complex points and has bends + 1 actual real affine segments. eval i t tests every real t in [0,1]; support is their union. IsSimple permits equal global parameters at adjacent junctions and first/last endpoint closure, excluding all other contacts. A one-segment loop therefore fails simplicity:

open Cslib.Polygonal in
example (z : ℂ) : ¬(Route.line z z).IsSimple := byz:ℂ⊢ ¬(Route.line z z).IsSimple
  rw [Route.isSimple_line_iffz:ℂ⊢ ¬z ≠ z]z:ℂ⊢ ¬z ≠ z
  exact not_not.mpr rflAll goals completed! 🐙

Graph.PolygonalDrawing G uses the existing natural-number vertex names and listed edge occurrences. Its data are vertex coordinates, one route per edge position and endpoint equations; it stores no numerical genus or geometry provider. IsEmbedding requires distinct declared names to have distinct points, simple routes, declared-vertex contacts only at their corresponding ends, and contacts of different routes only at common named ends. Undeclared names are unconstrained. Repeated declarations name the same point; identical edge pairs keep separate routes; a loop retains two end parameters and outgoing germs.

open Cslib.Complexity Graph in
example : (PolygonalDrawing.star 20).IsEmbedding :=
  PolygonalDrawing.star_isEmbedding 20

open Cslib.Complexity Graph in
example (r : RotationSystem ⟨[7, 7, 100], []⟩) :
    (PolygonalDrawing.points [7, 7, 100]).IsEmbedding ∧
      (PolygonalDrawing.points [7, 7, 100]).Realizes r :=
  ⟨PolygonalDrawing.points_isEmbedding _,
    PolygonalDrawing.points_realizes _ r⟩

star_isEmbedding n works at every degree, including zero. It asserts no arbitrary-degree star realization theorem. points_realizes covers every rotation of the edgeless graph, including sparse and repeated declarations. For any embedding, equal directions at one vertex force equal darts, even when the darts are the two ends of one loop:

open Cslib.Complexity Graph in
example {G : Graph} {D : PolygonalDrawing G} (hD : D.IsEmbedding)
    (a b : Dart G) (hv : a.vertex = b.vertex)
    (hdir : D.direction a = D.direction b) : a = b :=
  hD.directions_injective a b hv hdir

IsEmbedding.exists_vertex_ball hD v hv constructs a positive-radius ball about a declared vertex. Every route segment meeting that ball is a first segment starting at v or a last segment ending at v. The proof separates finitely many compact real segments internally; it supplies neither a topological disk theorem nor a vertex-splitting patch.

PolygonalDrawing.Realizes r is separate from IsEmbedding. It requires nonzero germs, injective incident directions and, for distinct incident a,b,c, the literal equivalence sbtw (D.direction c) (D.direction b) (D.direction a) ↔ b ∈ r.rotationInterval a c. Reversing Mathlib's counterclockwise angle betweenness makes forward rotate clockwise in the fixed complex plane; reflection is not allowed. The existing faceNext = rotate⁻¹ ∘ reversal (σ⁻¹ α) retains its right-side face convention.

The extracted ClosedPassages.loop e he pairs the two actual ends of a listed loop, with support fun i => decide (i = e). The numerical noninterlacing corollary retains the explicit declared-endpoint guard hG:

open Cslib.Complexity Graph in
example {G : Graph} (r : RotationSystem G)
    (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.1)
    (hr : r.NumericalGenusZero) (e f : Fin G.2.length) (hef : e ≠ f)
    (he : (Dart.vertex (G := G) (e, false)) = Dart.vertex (e, true))
    (hf : (Dart.vertex (G := G) (f, false)) = Dart.vertex (f, true)) :
    ¬r.Alternates (e, false) (e, true) (f, false) (f, true) :=
  r.not_alternates_loops hG hr e f hef he hf

This needs no connectedness or degree bound and constructs no drawing. CslibFrontierTests/PolygonalDrawing.lean checks actual bridge, closed-loop and parallel-digon realizations, star embeddings at degrees 0, 5 and 20, sparse isolates, clockwise sign and reverse-order rejection. CslibFrontierTests/PolygonalDrawingAudit.lean audits stored declarations and environment linters; CslibFrontierTests/RotationIntersection.lean uses the extracted loop constructor in finite parity clients. These are original geometric constructions, with no DK, FKP or Hanani–Tutte formalization, coordinate bit bound or native runtime claim.

2.17.1. Loop-only Forward Realization🔗

Import CslibFrontier.Computability.Complexity.Problems.Graph.RotationSystem.Realization.Bouquet. Every listed edge must be a loop. Declared endpoints and numerical genus zero then suffice for an actual embedding realizing the exact given clockwise rotation, with no noncrossing or geometric provider premise:

open Cslib.Complexity Graph in
example {G : Graph} (r : RotationSystem G)
    (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.1)
    (hr : r.NumericalGenusZero)
    (hloop : ∀ e : Fin G.2.length,
      (Dart.vertex (G := G) (e, false)) = Dart.vertex (e, true)) :
    ∃ D : PolygonalDrawing G, D.IsEmbedding ∧ D.Realizes r :=
  r.exists_polygonalDrawing_of_loops hG hr hloop

This includes sparse or repeated declarations and disconnected isolates. Here the actual two-loop certificate supplies the numerical premise:

open Cslib.Complexity Graph in
example : ∃ D : PolygonalDrawing
    ⟨[7, 7, 1000], [(7, 7), (7, 7)]⟩, D.IsEmbedding := by⊢ ∃ D, D.IsEmbedding
  let G : Graph := ⟨[7, 7, 1000], [(7, 7), (7, 7)]⟩G:Graph := { vertices := [7, 7, 1000], edges := [(7, 7), (7, 7)] }⊢ ∃ D, D.IsEmbedding
  let c : RotationCertificate := ⟨[2, 0, 3, 1]⟩G:Graph := { vertices := [7, 7, 1000], edges := [(7, 7), (7, 7)] }c:RotationCertificate := { successor := [2, 0, 3, 1] }⊢ ∃ D, D.IsEmbedding
  have hc : RotationCertificate.verifyRotation G c = true := by decideG:Graph := { vertices := [7, 7, 1000], edges := [(7, 7), (7, 7)] }c:RotationCertificate := { successor := [2, 0, 3, 1] }hc:RotationCertificate.verifyRotation G c = true⊢ ∃ D, D.IsEmbedding
  let r := RotationCertificate.decode G c hcG:Graph := { vertices := [7, 7, 1000], edges := [(7, 7), (7, 7)] }c:RotationCertificate := { successor := [2, 0, 3, 1] }hc:RotationCertificate.verifyRotation G c = truer:G.RotationSystem := RotationCertificate.decode G c hc⊢ ∃ D, D.IsEmbedding
  have hr : r.NumericalGenusZero :=
    (RotationCertificate.verifyEuler_eq_true_iff hc).mp (byG:Graph := { vertices := [7, 7, 1000], edges := [(7, 7), (7, 7)] }c:RotationCertificate := { successor := [2, 0, 3, 1] }hc:RotationCertificate.verifyRotation G c = truer:G.RotationSystem := RotationCertificate.decode G c hc⊢ RotationCertificate.verifyEuler G c = true decideAll goals completed! 🐙)G:Graph := { vertices := [7, 7, 1000], edges := [(7, 7), (7, 7)] }c:RotationCertificate := { successor := [2, 0, 3, 1] }hc:RotationCertificate.verifyRotation G c = truer:G.RotationSystem := RotationCertificate.decode G c hchr:r.NumericalGenusZero⊢ ∃ D, D.IsEmbedding
  obtain ⟨D, hD, _⟩ :=
    r.exists_polygonalDrawing_of_loops (byG:Graph := { vertices := [7, 7, 1000], edges := [(7, 7), (7, 7)] }c:RotationCertificate := { successor := [2, 0, 3, 1] }hc:RotationCertificate.verifyRotation G c = truer:G.RotationSystem := RotationCertificate.decode G c hchr:r.NumericalGenusZero⊢ ∀ v ∈ G.incidenceVertices, v ∈ G.vertices decideAll goals completed! 🐙) hr (byG:Graph := { vertices := [7, 7, 1000], edges := [(7, 7), (7, 7)] }c:RotationCertificate := { successor := [2, 0, 3, 1] }hc:RotationCertificate.verifyRotation G c = truer:G.RotationSystem := RotationCertificate.decode G c hchr:r.NumericalGenusZero⊢ ∀ (e : Fin G.edges.length), Dart.vertex (e, false) = Dart.vertex (e, true) decideAll goals completed! 🐙)G:Graph := { vertices := [7, 7, 1000], edges := [(7, 7), (7, 7)] }c:RotationCertificate := { successor := [2, 0, 3, 1] }hc:RotationCertificate.verifyRotation G c = truer:G.RotationSystem := RotationCertificate.decode G c hchr:r.NumericalGenusZeroD:G.PolygonalDrawinghD:D.IsEmbeddingright✝:D.Realizes r⊢ ∃ D, D.IsEmbedding
  exact ⟨D, hD⟩All goals completed! 🐙

PolygonalDrawing.bouquet r hloop is the explicit drawing. Each loop has five affine segments, with radial ports ranked in literal clockwise order. Numerical nonalternation supplies disjoint or nested port intervals; the construction proves actual real-parameter nonintersection internally. CslibFrontierTests/PolygonalBouquet.lean also checks a nonvacuous unbounded-degree family, nested/disjoint loops, interlacing obstruction and reversed-order rejection. This loop-only theorem supplies the base of the general forward construction. No coordinate-bit or native-runtime claim is made.

2.17.2. General Forward Realization and Restoration🔗

Ordinary import CslibFrontier.Computability.Complexity.Problems.Graph.RotationSystem.Realization.Forward gives the provider-free theorem for every supplied rotation:

open Cslib.Complexity Graph in
example {G : Graph} (r : RotationSystem G)
    (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.1)
    (hr : r.NumericalGenusZero) :
    ∃ D : PolygonalDrawing G, D.IsEmbedding ∧ D.Realizes r :=
  r.exists_polygonalDrawing hG hr

There is no degree, connectedness, loop, bridge, cofaciality, rational-coordinate or geometric-provider premise. In particular, every nonloop star degree is included, using the numerical star API imported at the start of this chapter:

open Cslib.Complexity Graph Graph.RotationSystem in
example (n : ℕ) : ∃ D : PolygonalDrawing (starGraph n),
    D.IsEmbedding ∧ D.Realizes (starRotation n) :=
  (starRotation n).exists_polygonalDrawing (starGraph_endpoints_declared n)
    (numericalGenusZero_starRotation n)

The proof reindexes a nonloop occurrence, contracts it, recurses on edge count, restores it and transports back to the exact original edge/declaration lists. Ordinary Realization.Restoration imports also expose complete restoration of any supplied actual contracted drawing:

open Cslib.Complexity Graph Graph.RotationSystem in
example {G : Graph} {u v : ℕ}
    (r : RotationSystem (lastEdgeGraph G u v)) (huv : u ≠ v)
    (hG : ∀ w ∈ (lastEdgeGraph G u v).incidenceVertices, w ∈ G.1)
    {D : PolygonalDrawing (contractLastEdgeGraph G u v)}
    (hD : D.IsEmbedding) (hR : D.Realizes (r.contractLastEdge huv)) :
    ∃ ρ > 0, ∃ a b : ℂ, (D.restoration huv ρ a b).IsEmbedding ∧
      (D.restoration huv ρ a b).Realizes r :=
  hR.exists_restoration r huv hG hD

The radius, centers, separated fans and exact connector insertion gaps are chosen internally. Exterior pieces remain, and both ends of a target loop reattach independently. Empty retained blocks keep their prescribed slots; all real contacts, simplicity, declared points and clockwise triples are proved. The generic rank API lives in RotationSystem.IntervalOrder; ordinary Realization.BouquetOrder imports continue to expose it without aliases.

CslibFrontierTests/PolygonalForward.lean applies the theorem to bridges, parallel occurrences, endpoint loops, untouched components, sparse repeated declarations, isolates and emptiness. PolygonalContractionSplit.lean applies automatic restoration to an actual drawing with two independent loop ends. PolygonalJoin, PolygonalRestriction and PolygonalSplitFans check local APIs.

2.17.3. Polygonal-to-Numerical Converse🔗

Ordinary import CslibFrontier.Computability.Complexity.Problems.Graph.RotationSystem.Realization.Converse supplies the arbitrary finite PL direction, on the existing genuine drawing and numerical models:

open Cslib.Complexity Graph in
example {G : Graph} {D : PolygonalDrawing G} {r : RotationSystem G}
    (hD : D.IsEmbedding) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.1)
    (hR : D.Realizes r) : r.NumericalGenusZero :=
  hD.numericalGenusZero hG hR

There is no genus, face-color, disk, Jordan or HT provider. The proof retains all real segment parameters, both loop ends, indexed parallel occurrences, arbitrary degree, sparse/duplicate declarations, disconnected components and points. Endpoint declarations remain explicit.

The actual intermediate colors are also available to clients:

open Cslib.Complexity Graph in
example {G : Graph} {D : PolygonalDrawing G} {r : RotationSystem G}
    (hD : D.IsEmbedding) (hR : D.Realizes r)
    (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.1)
    (x : Fin G.2.length → Bool) (hx : G.VertexEven x) :
    ∃ q : r.Face → Bool, r.faceBoundary q = x :=
  hD.exists_faceColors hR hG x hx

Right-side ray values transport through actual segments and bends, then through the empty literal clockwise vertex sectors. They descend to the existing face quotient. The indexed-dual/lifting exactness criterion supplies Euler equality; its face-color premise is discharged internally in the final theorem.

Ordinary Realization.Equivalence imports combine the general endpoints:

open Cslib.Complexity Graph in
example {G : Graph} (r : RotationSystem G)
    (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.1) :
    r.NumericalGenusZero ↔
      ∃ D : PolygonalDrawing G, D.IsEmbedding ∧ D.Realizes r :=
  r.numericalGenusZero_iff_exists_polygonalDrawing hG

Use .mp hr for the forward construction and .mpr ⟨D, hD, hR⟩ for the converse. CslibFrontierTests/PolygonalEquivalence.lean checks both directions through this ordinary import on nonloop stars at arbitrary degree.

A failure of numerical genus excludes that specific realized rotation:

open Cslib.Complexity Graph in
example {G : Graph} (r : RotationSystem G)
    (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.1)
    (hbad : ¬r.NumericalGenusZero) :
    ¬∃ D : PolygonalDrawing G, D.IsEmbedding ∧ D.Realizes r := byG:Graphr:G.RotationSystemhG:∀ v ∈ G.incidenceVertices, v ∈ G.verticeshbad:¬r.NumericalGenusZero⊢ ¬∃ D, D.IsEmbedding ∧ D.Realizes r
  rintro ⟨D, hD, hR⟩G:Graphr:G.RotationSystemhG:∀ v ∈ G.incidenceVertices, v ∈ G.verticeshbad:¬r.NumericalGenusZeroD:G.PolygonalDrawinghD:D.IsEmbeddinghR:D.Realizes r⊢ False
  exact hbad (hD.numericalGenusZero hG hR)All goals completed! 🐙

This does not assert nonplanarity of the underlying graph. The complete CslibFrontierTests/PolygonalConverse.lean applies the endpoint to actual loop, bridge, parallel-digon and degree-five clockwise star drawings; it also checks nonzero loop face colors, sparse/duplicate points, emptiness and a torus rotation obstruction. PolygonalConverseAudit.lean records scoped stored declaration/axiom/environment checks.

These are original finite PL proofs. Arbitrary topological-arc taming, indexed FZ versus DK set source comparison, frozen-switch completeness, Hanani–Tutte, bare recognition and full #3091 remain open. No coordinate-bit, runtime/P bound or CSP dichotomy is claimed.