PictureBoundaryParity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.HyperbolicObstruction.PictureSwitch.perm_transition_not_unique line 20
Source documentation
A cyclic word cannot have just one change of color. The colors need not be Boolean; the proof counts the occurrences of the color at the exceptional position. This is the literal rotation-system boundary conservation law.
```
lemma perm_transition_not_unique {C : Type*} (p : Perm D) (color : D → C) (x : D)
    (hx : color (p x) ≠ color x) :
    ∃ y : D, y ≠ x ∧ p.SameCycle x y ∧ color (p y) ≠ color y := by
…
```
theorem OAI.HyperbolicObstruction.PictureSwitch.PictureMap.boundary_dart_not_unique line 61
Source documentation
If a coloring is constant around faces, every vertex incident to a color-boundary edge has at least TWO distinct incident boundary darts. Parallel edges and loops are retained; there is no simple-graph assumption.
```
theorem boundary_dart_not_unique {C : Type*} (color : D → C)
    (hface : ∀ x, color (M.face x) = color x) (x : D)
    (hx : color (M.edge x) ≠ color x) :
    ∃ y : D, y ≠ x ∧ M.vertexClass y = M.vertexClass x ∧
      color (M.edge y) ≠ color y := by
…
```