ContourEnumeration.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The explicit C(m+1)^2 4^m encoding bound from cr:oriented-paths.

theorem OAI.PlanarFPP.SquareLoop.eq_of_start_direction line 12
Also declared: OAI/Probability/FirstPassage/ContourEnumeration.lean:11 (same declaration text).
abbrev OAI.PlanarFPP.EnclosingLoop line 47
Source documentation
Length n+1 avoids a spurious zero-length contour in the countable union.
Also declared: OAI/Probability/FirstPassage/ContourEnumeration.lean:45 (same declaration text).
```
abbrev EnclosingLoop (n : ℕ) :=
…
```
def OAI.PlanarFPP.enclosingLoopCode line 50
Distinct definitions of this name: OAI/Probability/FirstPassage/ContourEnumeration.lean:48 (different declaration text). Qualify references as OAI.PlanarFPP.enclosingLoopCode@path.
theorem OAI.PlanarFPP.enclosingLoopCode_injective line 55
Also declared: OAI/Probability/FirstPassage/ContourEnumeration.lean:53 (same declaration text).
instance OAI.PlanarFPP.enclosingLoopFintype line 63
Also declared: OAI/Probability/FirstPassage/ContourEnumeration.lean:61 (same declaration text).
theorem OAI.PlanarFPP.enclosingLoop_card line 68
Source documentation
At most 9(m+1)^2 4^m enclosing loops of length m = n+1, with indexed starting side; counting these also bounds unrooted contours.
Distinct definitions of this name: OAI/Probability/FirstPassage/ContourEnumeration.lean:64 (same statement text; different proof or body). Qualify references as OAI.PlanarFPP.enclosingLoop_card@path.
```
theorem enclosingLoop_card (n : ℕ) :
    Fintype.card (EnclosingLoop n) ≤ 9*(n+2)^2*4^(n+1) := by
…
```
Mentions: OAI.PlanarFPP.EnclosingLoop