Lifting face-even edge labels to vertex spins

The finite-field proof uses the actual indexed source and dual incidence matrices. Connectedness gives their ranks; componentwise Euler makes the included cut and face-kernel spaces have equal dimension. This finite-field argument is an original reconstruction.

[DK15], Section 3, Lemma 5 and Corollary 4 (printed p. 439), use differences on connected plane instances; the proof of Theorem 2 (printed p. 440) applies that correspondence to satisfiability. Here the statement is the graph-theoretic lifting prerequisite for arbitrary listed graphs and arbitrary edge bits. Its hypotheses are declared endpoints and the existing componentwise numerical Euler predicate. It asserts neither the cited CSP equivalence nor a geometric realization or native complexity bound. Spanning-cotree certificates, runtime oracles, and a finite natural-number universe are not assumed.

Main results

• Cslib.Complexity.Graph.RotationSystem.component_euler_le: the matrix Euler bound for an incident component, without a numerical genus hypothesis.
• Cslib.Complexity.Graph.RotationSystem.exists_vertexSpins_of_faceEven: disconnected lifting.
• Cslib.Complexity.Graph.RotationSystem.faceEven_iff_exists_vertexSpins: the exact parity test.
• Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_of_faceEven_lifts: its algebraic converse, with component restriction and zero extension discharged internally.

theorem Cslib.Complexity.Graph.RotationSystem.component_euler_le {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (d : G.Dart) : (G.componentVertexSet d.vertex).card + (r.componentFaceIndices d.vertex).card ≤ (G.componentEdgeSet d.vertex).card + 2

The actual vertices and face cycles of an incident component satisfy the Euler bound. This elementary consequence of the primal and dual incidence ranks needs neither numerical genus zero nor global connectedness. The supplied dart selects an incident component; this statement does not apply to isolated points or assert a geometric realization.

theorem Cslib.Complexity.Graph.RotationSystem.exists_vertexSpins_on_component {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hgenus : r.NumericalGenusZero) (x : Fin G.edges.length → Bool) (hx : r.FaceEven x) (d : G.Dart) : ∃ (spin : ℕ → Bool), ∀ i ∈ G.componentEdgeSet d.vertex, G.edgeGradient spin i = x i

Every face-even assignment lifts on each edge component, with all rank and dimension ingredients discharged internally from existing reachability and componentwise Euler.

theorem Cslib.Complexity.Graph.RotationSystem.numericalGenusZero_of_faceEven_lifts {G : Graph} (r : G.RotationSystem) (hG : ∀ v ∈ G.incidenceVertices, v ∈ G.vertices) (hlift : ∀ (x : Fin G.edges.length → Bool), r.FaceEven x → ∃ (spin : ℕ → Bool), G.edgeGradient spin = x) : r.NumericalGenusZero

Algebraic converse to face-even lifting: if every face-even edge labeling is a vertex gradient, the existing componentwise numerical Euler predicate holds. The component proof extends edge vectors by zero before applying the hypothesis and reuses the actual incidence ranks. Declared points use the separate conventional face and require no invented dart. This characterizes numerical genus zero and asserts no geometric realization.

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

Every face-even assignment on a componentwise numerically genus-zero indexed rotation lifts to spins on the original natural-number names. Components are solved independently; isolated declared points and names outside the graph may be assigned false.

theorem Cslib.Complexity.Graph.RotationSystem.faceEven_iff_exists_vertexSpins {G : Graph} (r : G.RotationSystem) (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

Face parity characterizes vertex gradients for arbitrary finite listed graphs under the existing componentwise numerical genus-zero predicate. The endpoint-declaration hypothesis is explicit. Loops, parallel occurrences, disconnected components, points, duplicate vertex declarations, and sparse natural-number names are all retained. The converse needs no genus assumption; see faceEven_edgeGradient.