BoundaryCycles.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Directed boundary cycles with nonzero signed ray-crossing count.

theorem OAI.PlanarFPP.exists_cycle_nonzero_sum line 12
Source documentation
A nonzero total weight on a fixed-point-free finite permutation has a cycle of nonzero weight.
Also declared: OAI/Probability/FirstPassage/BoundaryCycles.lean:9 (same declaration text).
```
theorem exists_cycle_nonzero_sum {α : Type*} [Fintype α] [DecidableEq α]
    (p : Equiv.Perm α) (hp : ∀ x, p x ≠ x) (w : α → ℤ)
    (hw : ∑ x, w x ≠ 0) :
    ∃ x, ∑ y ∈ (p.toList x).toFinset, w y ≠ 0 := by
…
```
theorem OAI.PlanarFPP.exists_boundary_cycle line 44
Source documentation
The source's enclosing boundary walk, with "nonzero winding" represented by its exact signed intersections with the positive horizontal ray.
Also declared: OAI/Probability/FirstPassage/BoundaryCycles.lean:39 (same declaration text).
```
theorem exists_boundary_cycle (S : Finset Vertex) (h0 : (0 : Vertex) ∈ S) :
    ∃ x : BoundarySide S,
      let es := (boundaryPerm S).toList x
…
```
Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.BoundarySide, OAI.PlanarFPP.boundaryPerm