PictureBoundaryHull.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.face_color_boundary_in_hull line 27
Source documentation
The topological separation mechanism behind the tree--cotree separator. A face coloring can change across tree edges only inside the root-path hull of its non-tree changes. Proof: literal vertex-rotation conservation gives two distinct boundary Dart copies at every unprotected boundary vertex; exact tree-copy uniqueness turns them into two distinct tree neighbors, contradicting a furthest-vertex argument.
```
theorem face_color_boundary_in_hull (hG : M.GenusZero)
    (hspan : SameCycle.setoid M.vertex ⊔ SameCycle.setoid q = ⊤)
    (hboundary : cycles (M.vertex*q) = 1)
    (root : M.GraphVertex) (S : Set M.GraphVertex)
    (hS : RootClosed (M.subpairingGraph q (M.subpairing_sq q hq)) root S)
    {C : Type*} (color : D → C) (hface : ∀ x, color (M.face x) = color x)
    (hother : ∀ x, q x = x → color (M.edge x) ≠ color x → M.vertexClass x ∈ S) :
    ∀ x, color (M.edge x) ≠ color x → M.vertexClass x ∈ S := by
…
```
Mentions: OAI.HyperbolicObstruction.PictureSwitch.cycles