Boolean potentials along actual face cycles

A face-even edge labeling is a difference of a Boolean potential at consecutive darts of the face permutation. This holds for every indexed rotation, including positive genus. These potentials are not vertex spins. The forward proof supplies actual finite permutation cycle graphs with internally proved numerical genus zero; no lifting provider is assumed. The reverse implication is telescoping on the full face quotient, including singleton faces.

theorem Cslib.Complexity.Graph.RotationSystem.exists_facePotential_of_faceEven {G : Graph} (r : G.RotationSystem) (x : Fin G.edges.length → Bool) (hx : r.FaceEven x) : ∃ (p : G.Dart → Bool), ∀ (d : G.Dart), x d.1 = (p d ^^ p (r.faceNext d))

Face-even labels have potentials on consecutive indexed face darts, with no genus or endpoint-declaration hypothesis. A dart potential need not descend to graph vertices.

theorem Cslib.Complexity.Graph.RotationSystem.faceEven_of_facePotential {G : Graph} (r : G.RotationSystem) (x : Fin G.edges.length → Bool) (p : G.Dart → Bool) (hp : ∀ (d : G.Dart), x d.1 = (p d ^^ p (r.faceNext d))) : r.FaceEven x

Differences of consecutive face-dart potentials telescope on every full face orbit. This implication also needs neither numerical genus nor declared endpoints.