Boolean cycles as boundaries of face colors

Vertex parity counts actual indexed darts: a loop contributes twice. Face boundaries take the exclusive or of the colors of the two actual incident face orbits. On a componentwise numerically genus-zero rotation, the vertex-even labels are exactly these boundaries.

This is an original finite reconstruction, obtained by applying the existing face-even lifting theorem to the actual indexed dual. It includes sparse and duplicate vertex declarations, parallel occurrences, loops, points, disconnected graphs and the empty graph. It asserts no geometric realization, Jordan theorem or Hanani–Tutte theorem.

Main definitions

• Cslib.Complexity.Graph.vertexParity: actual dart-incidence parity.
• Cslib.Complexity.Graph.RotationSystem.faceBoundary: boundary of actual face colors.

Main results

• Cslib.Complexity.Graph.RotationSystem.vertexEven_iff_exists_faceColors: cycle exactness.

noncomputable def Cslib.Complexity.Graph.vertexParity (G : Graph) (x : Fin G.edges.length → Bool) (v : ℕ) : Bool

Sum of edge bits over actual dart incidences at a natural-number vertex. Both ends of a loop occur, so their contributions cancel. Undeclared names with no darts have zero parity.

def Cslib.Complexity.Graph.VertexEven (G : Graph) (x : Fin G.edges.length → Bool) : Prop

Every vertex has even incidence parity, counting both indexed ends of every loop.

def Cslib.Complexity.Graph.RotationSystem.faceBoundary {G : Graph} (r : G.RotationSystem) (q : r.Face → Bool) : Fin G.edges.length → Bool

The boundary of face colors labels each edge by the exclusive or of its two incident actual face orbits. A bridge incident twice to one face consequently receives false.

theorem Cslib.Complexity.Graph.RotationSystem.faceBoundary_dart {G : Graph} (r : G.RotationSystem) (q : r.Face → Bool) (d : G.Dart) : r.faceBoundary q d.1 = (q ⟦d⟧ ^^ q ⟦d.reverse⟧)

Either end reads the same face boundary.

@[simp]

theorem Cslib.Complexity.Graph.RotationSystem.faceDualVertexEquiv_mk {G : Graph} (r : G.RotationSystem) (d : G.Dart) : ↑(r.faceDualVertexEquiv ⟦d⟧) = r.faceId d

The canonical face/dual-vertex equivalence sends a dart's face to its actual face ID.

theorem Cslib.Complexity.Graph.RotationSystem.dual_faceParity_eq_vertexParity {G : Graph} (r : G.RotationSystem) (x : Fin G.edges.length → Bool) (d : G.Dart) : r.dualRotation.faceParity (fun (i : Fin r.dualGraph.edges.length) => x (Fin.cast ⋯ i)) ⟦r.dualDartEquiv d⟧ = G.vertexParity x d.reverse.vertex

Dual-face parity is original vertex parity, with the reversal required by the actual dual face successor. No Euler or endpoint declaration assumption is needed.

theorem Cslib.Complexity.Graph.RotationSystem.vertexEven_iff_dual_faceEven {G : Graph} (r : G.RotationSystem) (x : Fin G.edges.length → Bool) : G.VertexEven x ↔ r.dualRotation.FaceEven fun (i : Fin r.dualGraph.edges.length) => x (Fin.cast ⋯ i)

Vertex-even labels are precisely face-even labels on the actual indexed dual.

theorem Cslib.Complexity.Graph.RotationSystem.dual_edgeGradient_faceColors {G : Graph} (r : G.RotationSystem) (q : r.Face → Bool) : ∃ (spin : ℕ → Bool), r.dualGraph.edgeGradient spin = fun (i : Fin r.dualGraph.edges.length) => r.faceBoundary q (Fin.cast ⋯ i)

A face boundary becomes the ordinary endpoint gradient on the actual indexed dual.

theorem Cslib.Complexity.Graph.RotationSystem.vertexEven_faceBoundary {G : Graph} (r : G.RotationSystem) (q : r.Face → Bool) : G.VertexEven (r.faceBoundary q)

Every face boundary has even incidence parity, with no genus or endpoint assumptions.

theorem Cslib.Complexity.Graph.RotationSystem.vertexEven_iff_exists_faceColors {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hgenus : r.NumericalGenusZero) (x : Fin G.edges.length → Bool) : G.VertexEven x ↔ ∃ (q : r.Face → Bool), r.faceBoundary q = x

Under declared endpoints and componentwise numerical genus zero, every vertex-even Boolean edge label is a boundary of actual face colors, and conversely. The quantifiers include arbitrary disconnected supports, loops, parallels, sparse names, duplicate declared vertices, isolated points and empty graphs. This is finite map mathematics, not a geometric planarity or Hanani–Tutte statement.