Ray parity on the actual segments of a polygonal drawing

Vertex-even edge labels induce even incidence at every actual segment endpoint: internal bends cancel in pairs and the original endpoints sum to Graph.vertexParity. A single complex rotation and positive scaling makes every nondegenerate segment nonhorizontal. The generic finite-arrangement theorem then makes the selected ray parity locally constant off its actual support, including all endpoint heights and arbitrary coincident bends.

These are original finite calculations. Local constancy alone does not identify the right-side samples of a rotation's face successor, and no colors on RotationSystem.Face or numerical-genus converse are asserted here.

@[reducible, inline]

abbrev Cslib.Complexity.Graph.PolygonalDrawing.SegmentIndex {G : Graph} (D : G.PolygonalDrawing) : Type

An actual listed segment, retaining its edge occurrence and its position on that route.

def Cslib.Complexity.Graph.PolygonalDrawing.segmentStart {G : Graph} (D : G.PolygonalDrawing) (s : D.SegmentIndex) : ℂ

First listed point of an actual segment.

def Cslib.Complexity.Graph.PolygonalDrawing.segmentFinish {G : Graph} (D : G.PolygonalDrawing) (s : D.SegmentIndex) : ℂ

Second listed point of an actual segment.

theorem Cslib.Complexity.Graph.PolygonalDrawing.segment_endpoints_even {G : Graph} (D : G.PolygonalDrawing) (x : Fin G.edges.length → Bool) (hx : G.VertexEven x) (u p : ℂ) : ∑ s : D.SegmentIndex, ((if u * D.segmentStart s = p then x s.fst else 0) + if u * D.segmentFinish s = p then x s.fst else 0) = false

Even incidence on original indexed darts remains even on all actual segment endpoints. Both loop ends and repeated edge occurrences are retained. Internal bends contribute twice, including when different listed bends have coincident coordinates. No endpoint-declaration, simplicity, connectedness, degree or coordinate assumption is needed for this identity.

theorem Cslib.Complexity.Graph.PolygonalDrawing.IsEmbedding.exists_rayParity_locally_constant {G : Graph} {D : G.PolygonalDrawing} (hD : D.IsEmbedding) : ∃ (u : ℂ), u ≠ 0 ∧ ∀ (x : Fin G.edges.length → Bool), G.VertexEven x → ∀ (z : ℂ), (∀ (s : D.SegmentIndex), x s.fst = true → z ∉ segment ℝ (u * D.segmentStart s) (u * D.segmentFinish s)) → ∀ᶠ (w : ℂ) in nhds z, Polygonal.rayParity (fun (s : D.SegmentIndex) => u * D.segmentStart s) (fun (s : D.SegmentIndex) => u * D.segmentFinish s) (fun (s : D.SegmentIndex) => x s.fst) w = Polygonal.rayParity (fun (s : D.SegmentIndex) => u * D.segmentStart s) (fun (s : D.SegmentIndex) => u * D.segmentFinish s) (fun (s : D.SegmentIndex) => x s.fst) z

A genuine polygonal embedding admits a single ray direction for which every even edge label gives locally constant parity on the complement of its selected actual segments. The multiplier is chosen from the drawing alone, before the edge label or observation point. This is a local geometric theorem, not yet transport along the right side of a face walk.