2.18. Ordered Incidence-to-Polygon Rotations🔗

Import CslibFrontier.Computability.Complexity.Problems.CSP.RotationSystem.Primal.Euler. The actual polygonGraph puts one edge between successive variables of each cyclic scope, retaining occurrence positions and dense variable names. Unary scopes become loops; repeated names and identical constraints stay distinct. Given an incidence rotation respecting the original argument order, every polygon face is an indexed constraint face or an original incidence face:

open Cslib.Logic.PL Cslib.Complexity Cslib.Complexity.CSP in
noncomputable example {Rel V : Type} [DecidableEq V] (F : CSP Rel V)
    (r : Graph.RotationSystem (incidenceGraph F))
    (hOrder : RespectsArgumentOrder r)
    (hPos : ∀ i : Fin F.length, 0 < F[i.val].2.length) :
    (polygonRotation r).Face ≃ Fin F.length ⊕ r.Face :=
  polygonFaceEquiv r hOrder hPos

Singleton face orbits are included. With positive actual scopes, components correspond and the exact per-component counts preserve numerical genus zero:

open Cslib.Logic.PL Cslib.Complexity Cslib.Complexity.CSP in
example {Rel V : Type} [DecidableEq V] (F : CSP Rel V)
    (r : Graph.RotationSystem (incidenceGraph F))
    (hOrder : RespectsArgumentOrder r)
    (hPos : ∀ i : Fin F.length, 0 < F[i.val].2.length) :
    (polygonRotation r).NumericalGenusZero ↔ r.NumericalGenusZero :=
  numericalGenusZero_polygon_iff r hOrder hPos

The graph has exactly one edge per occurrence and at most that many variable vertices. The bridge covers empty/disconnected bodies and sparse names; positivity is about actual scopes and assumes no relation semantics or arity contract. Nullary constraints require separate handling. CslibFrontierTests/CSPPrimalRotation.lean checks loops, repeated positions, identical constraints, malformed arity, the positivity guard and a toroidal rotation. The finite graph is explicit; abstract rotation inverses and face bijections are proof data. The checked compiler below supplies an executable reduction. Geometric realization, bare recognition and the planar solver remain open.