RePairing.lean`

43 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Release075.PermCycles.cycleCount_mul_comm line 10
theorem OAI.Release075.PermCycles.components_comm line 14
theorem OAI.Release075.PermCycles.componentCount_comm line 17
theorem OAI.Release075.PermCycles.PlanarMap.symm line 20
theorem OAI.Release075.PermCycles.PlanarMap.swap_left line 26
Source documentation
Cutting a cycle does not create positive genus. The component split is proved, not presumed from a drawing.
```
theorem PlanarMap.swap_left {f g : Perm A} (hp : PlanarMap f g) {a b : A}
    (hab : f.SameCycle a b) : PlanarMap (Equiv.swap a b * f) g := by
…
```
Mentions: OAI.Release075.PermCycles.PlanarMap
theorem OAI.Release075.PermCycles.PlanarMap.swap_right line 62
theorem OAI.Release075.PermCycles.PlanarMap.join_left line 67
Source documentation
Joining two separate planar components along a chosen cycle slot is planar.
```
theorem PlanarMap.join_left {f g : Perm A} (hp : PlanarMap f g) {a b : A}
    (hab : ¬ components f g a b) : PlanarMap (Equiv.swap a b * f) g := by
…
```
Mentions: OAI.Release075.PermCycles.PlanarMap, OAI.Release075.PermCycles.components
theorem OAI.Release075.PermCycles.PlanarMap.join_right line 81
theorem OAI.Release075.PermCycles.swap_color_preserving line 88
theorem OAI.Release075.PermCycles.rePair_color line 105
theorem OAI.Release075.PermCycles.planar_rePair_allow line 114
theorem OAI.Release075.PermCycles.rePair_other_edge line 131
def OAI.Release075.PermCycles.dipoleFace line 139
Source documentation
Two oppositely oriented triangular faces.
```
noncomputable def dipoleFace : Perm (Fin 6) :=
…
```
theorem OAI.Release075.PermCycles.dipoleFace_zero line 142
theorem OAI.Release075.PermCycles.dipoleFace_one line 143
theorem OAI.Release075.PermCycles.dipoleFace_two line 144
theorem OAI.Release075.PermCycles.dipoleFace_three line 145
theorem OAI.Release075.PermCycles.dipoleFace_four line 146
theorem OAI.Release075.PermCycles.dipoleFace_five line 147
def OAI.Release075.PermCycles.dipoleReverse line 149
theorem OAI.Release075.PermCycles.dipoleReverse_zero line 152
theorem OAI.Release075.PermCycles.dipoleReverse_one line 153
theorem OAI.Release075.PermCycles.dipoleReverse_two line 154
theorem OAI.Release075.PermCycles.dipoleReverse_three line 155
theorem OAI.Release075.PermCycles.dipoleReverse_four line 156
theorem OAI.Release075.PermCycles.dipoleReverse_five line 157
theorem OAI.Release075.PermCycles.dipoleFace_count line 159
theorem OAI.Release075.PermCycles.range_invariant line 168
theorem OAI.Release075.PermCycles.components_rePair_le line 179

theorem OAI.Release075.PermCycles.isolate_dipole line 187

Source documentation

The actual two re-pairings isolate the cancellable six darts. This lemma retains arbitrary outside reconnections; it does not postulate an empty outside neighborhood. All unaffected face orbits, including the exterior, are unchanged.

theorem isolate_dipole {C : Type*} (r f : Perm A)
    (hi : Function.Involutive r) (hn : ∀ z, r z ≠ z)
    (color : A → C) (hc : ∀ z, color ((r*f) z) = color z)
    (e : Fin 6 ↪ A) (hf : ∀ j, f (e j) = e (dipoleFace j))
    (he : r (e 0) = e 3)
    (h10 : color (e 1) ≠ color (e 0)) (h21 : color (e 2) ≠ color (e 1))
    (h14 : color (e 1) = color (e 4)) (hp : PlanarMap r f) :
    ∃ r' : Perm A, Function.Involutive r' ∧ (∀ z, r' z ≠ z) ∧
      PlanarMap r' f ∧ (∀ z, color ((r'*f) z) = color z) ∧
      (∀ j, r' (e j) = e (dipoleReverse j)) ∧
      r' = rePair (rePair r (e 1) (e 5)) (e 2) (e 4) ∧
      components r' f ≤ components r f := by
…

Mentions: OAI.Release075.PermCycles.dipoleFace, OAI.Release075.PermCycles.PlanarMap, OAI.Release075.PermCycles.dipoleReverse, OAI.Release075.PermCycles.rePair, OAI.Release075.PermCycles.components

theorem OAI.Release075.PermCycles.cycleCount_delete_range line 288
Source documentation
Deleting an invariant finite family of face cycles has its exact effect on area; no ambient topological disk is presumed in the count.
```
theorem cycleCount_delete_range (f : Perm A) (t : Perm B) (e : B ↪ A)
    (he : ∀ b, f (e b) = e (t b)) :
    cycleCount f = cycleCount t + cycleCount
      (f.subtypePerm (p := fun a => a ∉ Set.range e)
…
```
Mentions: OAI.Release075.PermCycles.cycleCount
theorem OAI.Release075.PermCycles.rePair_labels line 303
theorem OAI.Release075.PermCycles.cancel_dipole line 311
theorem OAI.Release075.formPerm_append_cons line 349
theorem OAI.Release075.formPerm_concat line 359
def OAI.Release075.IsBoundary line 367
Source documentation
A specified exterior cycle, including the empty boundary. Its entries are incidences (darts), not necessarily distinct vertices or geometric edges.
```
def IsBoundary (f : Perm A) (l : List A) : Prop :=
…
```
theorem OAI.Release075.IsBoundary.mem_iff line 370
theorem OAI.Release075.IsBoundary.not_mem_iff line 384
theorem OAI.Release075.formPerm_embedding line 387
theorem OAI.Release075.IsBoundary.conjugate line 397
theorem OAI.Release075.IsBoundary.rotate line 406
theorem OAI.Release075.PermCycles.components_split_right_le line 420

theorem OAI.Release075.PermCycles.fold_pair line 438

Source documentation

Fold two consecutive inverse boundary incidences. Darts are first paired, then split off as their own isolated tree component. The surviving outside word is unchanged; no disjointness of the former outside partners is assumed.

theorem fold_pair {C E : Type*} (r f : Perm A)
    (hi : Function.Involutive r) (hn : ∀ a, r a ≠ a)
    (label : A → E) (flip : E → E) (hflip : Function.Involutive flip)
    (color : E → C) (hedge : ∀ e, color e ≠ color (flip e))
    (hl : ∀ a, label (r a) = flip (label a))
    (hc : ∀ a, color (label ((r*f) a)) = color (label a))
    (hp : PlanarMap r f) {a b : A} (hab : a ≠ b)
    (hf : f b = a) (he : label a = flip (label b)) :
    ∃ r' f' : Perm A,
      Function.Involutive r' ∧ (∀ z, r' z ≠ z) ∧ PlanarMap r' f' ∧
      (∀ z, label (r' z) = flip (label z)) ∧
      (∀ z, color (label ((r'*f') z)) = color (label z)) ∧
…

Mentions: OAI.Release075.PermCycles.PlanarMap