Componentwise Euler preservation for CSP polygons

Counts refer to the actual listed graphs and every face orbit, including singleton orbits. The target predicate is the existing componentwise NumericalGenusZero, with no change of model and no geometric, native-computation or recognition claim.

Main results

• Cslib.Complexity.CSP.polygon_component_vertex_count: exact variable/constraint split.
• Cslib.Complexity.CSP.polygon_component_edge_count: preserves indexed edge counts.
• Cslib.Complexity.CSP.polygon_component_face_card: complete component face counts.
• Cslib.Complexity.CSP.numericalGenusZero_polygon_iff: componentwise Euler equivalence.

theorem Cslib.Complexity.CSP.polygon_component_face_card {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (r : (incidenceGraph F).RotationSystem) (hOrder : RespectsArgumentOrder r) (hPos : ∀ (i : Fin (List.length F)), 0 < F[↑i].2.length) (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 }

In a component rooted at a dense variable, polygon faces are exactly its constraint positions together with its original incidence faces. All face orbits are counted.

theorem Cslib.Complexity.CSP.polygon_component_vertex_count {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (root : ℕ) (hr : root < F.numVars) : List.countP (fun (v : ℕ) => decide (Graph.RotationCertificate.SameComponent (incidenceGraph F) root v)) (incidenceGraph F).distinctVertices = List.countP (fun (v : ℕ) => decide (Graph.RotationCertificate.SameComponent (polygonGraph F) root v)) (polygonGraph F).distinctVertices + Nat.card { i : Fin (List.length F) // Graph.RotationCertificate.SameComponent (incidenceGraph F) root (F.numVars + ↑i) }

The incidence component has the polygon's variable vertices plus its indexed positive constraint vertices. Vertex names are counted once, while constraint positions stay distinct.

theorem Cslib.Complexity.CSP.polygon_component_edge_count {Rel V : Type} [DecidableEq V] {F : Logic.PL.CSP Rel V} (root : ℕ) (hr : root < F.numVars) : List.countP (fun (e : ℕ × ℕ) => decide (Graph.RotationCertificate.SameComponent (polygonGraph F) root e.1)) (polygonGraph F).edges = List.countP (fun (e : ℕ × ℕ) => decide (Graph.RotationCertificate.SameComponent (incidenceGraph F) root e.1)) (incidenceGraph F).edges

The component edge counts agree exactly: both lists retain one edge position per occurrence, and its first endpoint is the same dense variable.

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

Replacing every positive ordered incidence star by its actual occurrence-indexed polygon preserves the existing componentwise numerical genus-zero predicate in both directions. This includes disconnected and empty instances. It asserts no geometric realization.