Polygon Euler transport with nullary constraints

Nullary constraint vertices are isolated points in the original incidence graph. They add no polygon edge or face. Restricting the black face index to positive actual scopes extends the existing orbit correspondence without deleting or renumbering the original CSP. The numerical Euler transport below therefore applies to the original supplied certificate, even when true nullaries occur between positive constraints. Their truth is a separate semantic guard. No geometric embedding or recognition theorem is asserted.

@[reducible, inline]

abbrev Cslib.Complexity.CSP.PositiveConstraint {Rel V : Type} (F : Logic.PL.CSP Rel V) : Type

Indexed constraints having an actual argument; nullary positions have no black dart.

noncomputable def Cslib.Complexity.CSP.argumentOrbitPositiveEquiv {Rel V : Type} (F : Logic.PL.CSP Rel V) : Quotient (Equiv.Perm.SameCycle.setoid (argumentPermutation F)) ≃ PositiveConstraint F

The argument orbits are exactly the positive constraint positions, retaining duplicates.

noncomputable def Cslib.Complexity.CSP.polygonFacePositiveEquiv {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) : (polygonRotation r).Face ≃ PositiveConstraint F ⊕ r.Face

Complete face decomposition, with no positivity premise on the original CSP.

theorem Cslib.Complexity.CSP.polygonFacePositiveEquiv_black {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (o : F.Occurrence) : (polygonFacePositiveEquiv r hOrder) ⟦polygonDart o false⟧ = Sum.inl ⟨o.fst, ⋯⟩

The black face still has its exact original positive constraint index.

theorem Cslib.Complexity.CSP.polygonFacePositiveEquiv_white {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (o : F.Occurrence) : (polygonFacePositiveEquiv r hOrder) ⟦polygonDart ((Equiv.symm (argumentPermutation F)) o) true⟧ = Sum.inr ⟦incidenceDart o false⟧

The white correspondence is unchanged by isolated nullary constraint vertices.

theorem Cslib.Complexity.CSP.polygon_edge_faces_distinct_of_occurrence {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (o : F.Occurrence) : ⟦polygonDart o false⟧ ≠ ⟦polygonDart o true⟧

An edge always separates a black face from a distinct white face, regardless of nullaries.

theorem Cslib.Complexity.CSP.polygon_component_face_card_with_nullaries {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (root : ℕ) (hr : root < F.numVars) : Nat.card { f : (polygonRotation r).Face // ∃ (d : (polygonGraph F).Dart), Graph.RotationCertificate.SameComponent (polygonGraph F) root d.vertex ∧ ⟦d⟧ = f } = Nat.card { i : Fin (List.length F) // Graph.RotationCertificate.SameComponent (incidenceGraph F) root (F.numVars + ↑i) } + Nat.card { f : r.Face // ∃ (d : (incidenceGraph F).Dart), Graph.RotationCertificate.SameComponent (incidenceGraph F) root d.vertex ∧ ⟦d⟧ = f }

Nullary vertices are absent from every component rooted at an occurring variable.

theorem Cslib.Complexity.CSP.numericalGenusZero_polygon_with_nullaries {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (hgenus : r.NumericalGenusZero) : (polygonRotation r).NumericalGenusZero

Forward numerical Euler transport on the original instance, including every nullary constraint as an isolated incidence point. No deletion or supplied transport is assumed.