PlanarBoundary.lean`

53 declarations, 0 contain sorry, 0 declared as axioms

Oriented planar edge boundary with exact nearest-neighbor conventions.

abbrev OAI.PlanarBoundary.Point line 12
abbrev OAI.PlanarBoundary.Direction line 13
def OAI.PlanarBoundary.tailOffset line 15
def OAI.PlanarBoundary.headOffset line 16
def OAI.PlanarBoundary.outward line 17
abbrev OAI.PlanarBoundary.Boundary line 19
instance OAI.PlanarBoundary.(instance at line 21) line 21
def OAI.PlanarBoundary.tail line 25
def OAI.PlanarBoundary.head line 26
def OAI.PlanarBoundary.atVertex line 28
theorem OAI.PlanarBoundary.balanced line 45
Source documentation
At each dual vertex incoming and outgoing boundary degrees agree.
```
theorem balanced (X : Finset Point) (v : Point) :
    Fintype.card {e : Boundary X // head e = v} =
      Fintype.card {e : Boundary X // tail e = v} := by
…
```
Mentions: OAI.PlanarBoundary.Point, OAI.PlanarBoundary.Boundary, OAI.PlanarBoundary.head, OAI.PlanarBoundary.tail
theorem OAI.PlanarBoundary.head_ne_tail line 65
def OAI.PlanarBoundary.opposite line 71
theorem OAI.PlanarBoundary.opposite_opposite line 73
theorem OAI.PlanarBoundary.outward_opposite line 76
theorem OAI.PlanarBoundary.reverse_tail line 79
theorem OAI.PlanarBoundary.reverse_head line 82
def OAI.PlanarBoundary.rayFlux line 87
Source documentation
Signed intersections with the positive horizontal ray; dual vertex (a,b) represents the point (a-1/2,b-1/2).
```
def rayFlux (a b : Point) : ℤ :=
…
```
Mentions: OAI.PlanarBoundary.Point
theorem OAI.PlanarBoundary.rayFlux_reverse line 91
def OAI.PlanarBoundary.sideFlux line 95
theorem OAI.PlanarBoundary.sideFlux_reverse line 98
theorem OAI.PlanarBoundary.cell_flux line 106
Source documentation
The oriented boundary of one unit cell has ray intersection number one exactly when it contains the ray's origin. No Jordan curve theorem is assumed.
```
theorem cell_flux (cell : Point) :
    (∑ d : Direction, sideFlux cell d) = if cell = (0,0) then 1 else 0 := by
…
```
Mentions: OAI.PlanarBoundary.Point, OAI.PlanarBoundary.Direction, OAI.PlanarBoundary.sideFlux
abbrev OAI.PlanarBoundary.FullSide line 113
def OAI.PlanarBoundary.isInternal line 115
def OAI.PlanarBoundary.internalReverse line 117
theorem OAI.PlanarBoundary.internal_flux_zero line 133
def OAI.PlanarBoundary.boundaryEquiv line 146
theorem OAI.PlanarBoundary.boundary_flux line 154
Source documentation
The whole finite boundary has nonzero positive-ray intersection number.
```
theorem boundary_flux (X : Finset Point) :
    (∑ e : Boundary X, rayFlux (tail e) (head e)) = if (0,0) ∈ X then 1 else 0 := by
…
```
Mentions: OAI.PlanarBoundary.Point, OAI.PlanarBoundary.Boundary, OAI.PlanarBoundary.rayFlux, OAI.PlanarBoundary.tail, OAI.PlanarBoundary.head
def OAI.PlanarBoundary.Neighbor line 181
theorem OAI.PlanarBoundary.side_neighbor line 183
theorem OAI.PlanarBoundary.head_neighbor line 188
theorem OAI.PlanarBoundary.neighbor_coord line 191
def OAI.PlanarBoundary.lineFlux line 195
theorem OAI.PlanarBoundary.rayFlux_eq_lineFlux line 197
theorem OAI.PlanarBoundary.next_eq_rotate line 203
theorem OAI.PlanarBoundary.lineFlux_sum_zero line 208

theorem OAI.PlanarBoundary.two_sides line 214

Source documentation

Nonzero positive-ray flux forces a crossing on each side of the vertical axis.

theorem two_sides {n : ℕ} (hn : 0 < n) (v : Fin n → Point)
    (hedge : ∀ i, Neighbor (v i) (v (FiniteTrails.next hn i)))
    (hw : (∑ i, rayFlux (v i) (v (FiniteTrails.next hn i))) ≠ 0) :
    (∃ i, 0 < (v i).1 ∧ rayFlux (v i) (v (FiniteTrails.next hn i)) ≠ 0) ∧
      ∃ j, (v j).1 ≤ 0 := by
…

Mentions: OAI.PlanarBoundary.Point, OAI.PlanarBoundary.Neighbor, OAI.FiniteTrails.next, OAI.PlanarBoundary.rayFlux

theorem OAI.PlanarBoundary.coordinate_diameter line 231
Source documentation
A coarse diameter bound adequate for the same Peierls argument.
```
theorem coordinate_diameter {n : ℕ} (hn : 0 < n) (v : Fin n → Point)
    (hedge : ∀ i, Neighbor (v i) (v (FiniteTrails.next hn i))) (i j : Fin n) :
    (v i).1-(v j).1 < 2*(n : ℤ) := by
…
```
Mentions: OAI.PlanarBoundary.Point, OAI.PlanarBoundary.Neighbor, OAI.FiniteTrails.next
theorem OAI.PlanarBoundary.exists_anchored_trail line 260
Source documentation
Every finite region containing zero contains an edge-simple closed boundary trail with a positive-ray anchor of coordinate less than 2n. This deliberately uses a harmless overcount rather than an unformalized Jordan theorem.
```
theorem exists_anchored_trail (X : Finset Point) (hX : (0,0) ∈ X) :
    ∃ n : ℕ, ∃ hn : 0 < n, ∃ e : Fin n → Boundary X,
      Function.Injective e ∧
      (∀ i, tail (e (FiniteTrails.next hn i)) = head (e i)) ∧
      ∃ i, 0 < (tail (e i)).1 ∧ (tail (e i)).1 < 2*(n : ℤ) ∧
        rayFlux (tail (e i)) (head (e i)) ≠ 0 := by
…
```
Mentions: OAI.PlanarBoundary.Point, OAI.PlanarBoundary.Boundary, OAI.PlanarBoundary.tail, OAI.FiniteTrails.next, OAI.PlanarBoundary.head, OAI.PlanarBoundary.rayFlux
abbrev OAI.PlanarBoundary.Code line 292
def OAI.PlanarBoundary.anchor line 294
def OAI.PlanarBoundary.wordAt line 296
def OAI.PlanarBoundary.displacement line 299
def OAI.PlanarBoundary.tracePosition line 301
def OAI.PlanarBoundary.traceSide line 304
theorem OAI.PlanarBoundary.trace_succ line 307
theorem OAI.PlanarBoundary.trace_reconstruct line 311
def OAI.PlanarBoundary.shiftIndex line 337
theorem OAI.PlanarBoundary.shiftIndex_injective line 340
theorem OAI.PlanarBoundary.shiftIndex_next line 348
theorem OAI.PlanarBoundary.rayFlux_ne_zero_height line 355
theorem OAI.PlanarBoundary.card_code line 360
Source documentation
The finite deterministic code family has at most 4n4^n members.
```
theorem card_code (n : ℕ) : Fintype.card (Code n) = 4*n*4^n := by
…
```
Mentions: OAI.PlanarBoundary.Code
theorem OAI.PlanarBoundary.exists_boundary_code line 365
Source documentation
Every actual boundary supplies one of these finitely encoded trails.
```
theorem exists_boundary_code (X : Finset Point) (hX : (0,0) ∈ X) :
    ∃ n : ℕ, ∃ _hn : 0 < n, ∃ c : Code n, ∃ e : Fin n → Boundary X,
      Function.Injective e ∧ ∀ i, traceSide c i = (e i).val := by
…
```
Mentions: OAI.PlanarBoundary.Point, OAI.PlanarBoundary.Code, OAI.PlanarBoundary.Boundary, OAI.PlanarBoundary.traceSide