2.14. Indexed Duality and Boolean Difference Lifting🔗

Import CslibFrontier.Computability.Complexity.Problems.Graph.RotationSystem.Lifting for the complete graph entry point. The actual dual keeps listed edge positions, including loops and parallel occurrences, and gives every source face its least actual dart index as a vertex name. Its vertex permutation is the source face successor. Complete face/incident-vertex and component bijections establish:

open Cslib.Complexity in
example {G : Graph} (r : Graph.RotationSystem G)
    (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) :
    r.dualRotation.NumericalGenusZero ↔ r.NumericalGenusZero :=
  r.numericalGenusZero_dual_iff hG

The endpoint guard is essential. Isolated source vertices have no darts and are omitted by dualization; their conventional Euler equation is trivial. Empty and disconnected graphs, duplicate declarations and sparse names are covered. Face parity counts dart occurrences with boundary multiplicity. For an indexed Boolean edge assignment, all face parities vanish exactly when it is the endpoint XOR of vertex spins:

open Cslib.Complexity in
example {G : Graph} (r : Graph.RotationSystem G)
    (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices)
    (hgenus : r.NumericalGenusZero) (x : Fin G.edges.length → Bool) :
    r.FaceEven x ↔ ∃ spin : ℕ → Bool, G.edgeGradient spin = x :=
  r.faceEven_iff_exists_vertexSpins hG hgenus x

The proof discharges the characteristic-two incidence-rank and connectivity facts internally. The gradient-to-parity direction telescopes without either premise:

open Cslib.Complexity in
example {G : Graph} (r : Graph.RotationSystem G) (spin : ℕ → Bool) :
    r.FaceEven (G.edgeGradient spin) :=
  r.faceEven_edgeGradient spin

CslibFrontierTests/RotationDual.lean contains concrete bridge, loop, digon, torus and disconnected sparse-name cases. These are finite combinatorial results. The checked compiler below provides the native supplied-certificate CSP reduction, followed by the complete native edge solver below. Geometric realization, bare recognition and final planar assembly remain open.