Dipoles.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Release075.TriangleFilling.activeCount line 10
structure OAI.Release075.TriangleFilling.Dipole line 15
Source documentation
The six oriented incidences of two faces which cancel across their common edge. Outside partners may reconnect arbitrarily elsewhere in the filling.
```
structure Dipole {w : List E} (D : TriangleFilling flip color face w) where
…
```
Mentions: OAI.Release075.TriangleFilling
theorem OAI.Release075.TriangleFilling.Dipole.cancel line 28
Source documentation
A labeled cancellation decreases the number of active darts. The isolated pair remains harmlessly as a component disjoint from the prescribed boundary.
```
theorem Dipole.cancel {w : List E} {D : TriangleFilling flip color face w} (P : D.Dipole) :
    ∃ D' : TriangleFilling flip color face w, D'.activeCount < D.activeCount := by
…
```
Mentions: OAI.Release075.TriangleFilling
theorem OAI.Release075.TriangleFilling.exists_noDipole line 88
Source documentation
Minimizing active size, not an assumed reduced-diagram axiom, produces a filling with no cancellable adjacent labelled pair.
```
theorem exists_noDipole {w : List E} (h : Fillable flip color face w) :
    ∃ D : TriangleFilling flip color face w, IsEmpty D.Dipole := by
…
```
Mentions: OAI.Release075.Fillable, OAI.Release075.TriangleFilling
def OAI.Release075.PermCycles.triangleEmbedding line 107
def OAI.Release075.PermCycles.trianglePairEmbedding line 118
theorem OAI.Release075.PermCycles.trianglePairEmbedding_values line 148

theorem OAI.Release075.TriangleFilling.reverse_not_sameCycle line 166

Source documentation

A genuinely triangular face cannot use both orientations of one geometric edge: its three differently colored vertices and the endpoint matching forbid it.

theorem reverse_not_sameCycle (a : D.Dart) (ha : D.Active a) (hna : a ∉ D.boundary)
    (hf : ∀ a b c, face a b c → color a ≠ color b ∧ color b ≠ color c ∧ color c ≠ color a) :
    ¬ D.next.SameCycle a (D.reverse a) := by
…

theorem OAI.Release075.TriangleFilling.dipole_of_link_backtrack line 189

Source documentation

Internal reversal of a link walk creates a cancellable pair, when the face labels are determined by two consecutive sides.

theorem dipole_of_link_backtrack
    (hf : ∀ a b c, face a b c → color a ≠ color b ∧ color b ≠ color c ∧ color c ≠ color a)
    (hflip : ∀ e, flip (flip e) = e)
    (hmirror : ∀ a b c, face a b c → face (flip a) (flip c) (flip b))
    (hunique : ∀ a b c c', face a b c → face a b c' → c = c')
    (x : D.Dart) (hx : D.Active x) (hnx : x ∉ D.boundary)
    (hnb : (D.reverse*D.next) x ∉ D.boundary)
    (hback : D.label x = D.label ((D.reverse*D.next) ((D.reverse*D.next) x))) :
    Nonempty D.Dipole := by
…

theorem OAI.Release075.TriangleFilling.noDipole_link_reduced line 247
def OAI.Release075.CyclicLink.walk line 268
Source documentation
The actual link walk traced by successive corners, without assuming its image is simple. This is why reduced closed walks, rather than only cycles, are needed.
```
def walk (f : A → A) (label : A → V) (adj : ∀ a, G.Adj (label a) (label (f a)))
    (n : ℕ) (a : A) : G.Walk (label a) (label (f^[n] a)) :=
…
```
theorem OAI.Release075.CyclicLink.length_walk line 274
theorem OAI.Release075.CyclicLink.getVert_walk line 281
theorem OAI.Release075.CyclicLink.reduced_walk line 296

theorem OAI.Release075.CyclicLink.orbit_card_ge line 308

Source documentation

A finite corner orbit mapping without link reversals has at least the link's actual girth. No injectivity of the whole orbit image is needed.

theorem orbit_card_ge [Fintype A] (f : Equiv.Perm A) (label : A → V)
    (adj : ∀ a, G.Adj (label a) (label (f a)))
    (reduced : ∀ a, label a ≠ label (f (f a)))
    (k : ℕ) (hgirth : ∀ v (p : G.Walk v v), p.IsCycle → k ≤ p.length) (a : A) :
    k ≤ (PermCycles.orbit f a).card := by
…

Mentions: OAI.Release075.PermCycles.orbit