BoundaryGeometry.lean`

24 declarations, 0 contain sorry, 0 declared as axioms

The uncancelled, counterclockwise square sides in crossings.tex:cr:oriented-paths. A dual vertex p represents the actual point p - (1/2,1/2), so the square at the primal site q has lower-left corner q in these integer coordinates.

instance OAI.PlanarFPP.(instance at line 14) line 14
def OAI.PlanarFPP.Step.left line 18
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:14 (same declaration text).
def OAI.PlanarFPP.Step.right line 21
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:17 (same declaration text).
def OAI.PlanarFPP.Step.outward line 24
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:20 (same declaration text).
def OAI.PlanarFPP.Step.corner line 26
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:22 (same declaration text).
abbrev OAI.PlanarFPP.SquareSide line 29
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:25 (same declaration text).
def OAI.PlanarFPP.SquareSide.tail line 31
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:27 (same declaration text).
def OAI.PlanarFPP.SquareSide.head line 33
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:29 (same declaration text).
def OAI.PlanarFPP.IsBoundarySide line 35
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:31 (same declaration text).
instance OAI.PlanarFPP.(instance at line 38) line 38
def OAI.PlanarFPP.boundarySides line 41
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:37 (same declaration text).
theorem OAI.PlanarFPP.mem_boundarySides line 44
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:40 (same declaration text).
def OAI.PlanarFPP.boundaryNext line 50
Source documentation
Follow the first uncancelled side counterclockwise around the arriving corner. The two tests inspect the other two squares meeting that corner.
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:44 (same declaration text).
```
def boundaryNext (S : Finset Vertex) (e : SquareSide) : SquareSide :=
…
```
Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.SquareSide
def OAI.PlanarFPP.boundaryPrev line 57
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:51 (same declaration text).
theorem OAI.PlanarFPP.boundaryNext_boundary line 64
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:58 (same declaration text).
theorem OAI.PlanarFPP.boundaryNext_tail line 79
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:73 (same declaration text).
theorem OAI.PlanarFPP.boundaryPrev_next line 91
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:85 (same declaration text).
abbrev OAI.PlanarFPP.BoundarySide line 104
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:98 (same declaration text).
def OAI.PlanarFPP.boundarySuccessor line 106
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:100 (same declaration text).
theorem OAI.PlanarFPP.boundarySuccessor_injective line 110
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:104 (same declaration text).
def OAI.PlanarFPP.boundaryPerm line 121
Source documentation
Cancellation of shared sides leaves a permutation of the remaining sides; its cycles are directed closed walks with no repeated directed side.
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:113 (same declaration text).
```
noncomputable def boundaryPerm (S : Finset Vertex) : Equiv.Perm (BoundarySide S) :=
…
```
Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.BoundarySide
theorem OAI.PlanarFPP.boundaryPerm_tail line 126
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:118 (same declaration text).
theorem OAI.PlanarFPP.boundaryPerm_ne_self line 129
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:121 (same declaration text).
theorem OAI.PlanarFPP.boundary_dualEdge_injective line 142
Source documentation
An unoriented dual edge cannot occur twice among uncancelled sides: its two possible orientations have opposite occupied and unoccupied cells.
Also declared: OAI/Probability/FirstPassage/BoundaryGeometry.lean:132 (same declaration text).
```
theorem boundary_dualEdge_injective (S : Finset Vertex) (e f : SquareSide)
    (he : IsBoundarySide S e) (hf : IsBoundarySide S f)
    (hh : e.2.edge e.tail = f.2.edge f.tail) : e = f := by
…
```
Mentions: OAI.PlanarFPP.Vertex, OAI.PlanarFPP.SquareSide, OAI.PlanarFPP.IsBoundarySide