Dart successor preserves the left face
ProvedDartSuccessorPreservesFacegraph-theoryplanar-graphs
For a crossing-free ordinary polygonal drawing equipped with plane face data, the successor permutation preserves the face on the left of every dart. Consequently, if a dart has left face , then every forward and backward iterate of the successor permutation also has left face ; the darts incident with any fixed face are unions of successor orbits.
Preamble
import Definitions.Def_PlaneFaceData open Classical noncomputable section
Formal statement
lemma DartSuccessorPreservesFace {V : Type*} [Fintype V] (G : SimpleGraph V)
[Fintype G.edgeSet] [DecidableRel G.Adj] (D : OrdinaryPolygonalDrawing G)
(hD : D.crossingSet.card = 0) (A : PlaneFaceData G D) :
(∀ d : G.Dart, A.leftFace (A.successor d) = A.leftFace d) ∧
∀ F : A.Face, ∀ d : G.Dart, A.leftFace d = F →
(∀ n : ℕ, A.leftFace ((A.successor^[n]) d) = F) ∧
∀ n : ℕ, A.leftFace (((A.successor.symm)^[n]) d) = F := by sorrySource