OAI/GroupTheory/Hyperbolic/TriangleFilling.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Release075.TriangleFilling line 12

   Source documentation

   A finite genus-zero map with a prescribed exterior walk. Other components are allowed but ignored; only the component meeting the boundary must be filled. This handles components detached by folds, spurs, and empty boundary words.

   structure TriangleFilling {E V : Type} (flip : E → E) (color : E → V)
       (face : E → E → E → Prop) (w : List E) where
   …

2. def OAI.Release075.TriangleFilling.empty line 35
3. def OAI.Release075.TriangleFilling.rotate line 51
4. theorem OAI.Release075.PermCycles.PlanarMap.involution line 80
5. def OAI.Release075.TriangleFilling.backtrack line 94
6. theorem OAI.Release075.IsBoundary.step line 120
7. theorem OAI.Release075.IsBoundary.erase_pair line 125
8. theorem OAI.Release075.same_outside_boundary_pow line 159
9. theorem OAI.Release075.PermCycles.components_pred line 179
10. theorem OAI.Release075.PermCycles.pair_invariant line 188
11. theorem OAI.Release075.TriangleFilling.fold line 207

    Source documentation

    A genuine reverse-edge deletion, retaining the external word even when the outside partners reconnect. The detached tree is an ignored separate component.

    theorem fold {w : List E} (D : TriangleFilling flip color face w)
        (hflip : Function.Involutive flip) (hne : ∀ e, color e ≠ color (flip e))
        {a b : D.Dart} {l : List D.Dart} (hb : D.boundary = b::a::l)
        (hl : D.label a = flip (D.label b)) :
        Nonempty (TriangleFilling flip color face (l.map D.label)) := by
    …

    Mentions: OAI.Release075.TriangleFilling

12. theorem OAI.Release075.IsBoundary.join line 262
13. theorem OAI.Release075.IsBoundary.swap_outside line 276
14. def OAI.Release075.TriangleFilling.Active line 292
15. theorem OAI.Release075.TriangleFilling.active_iff_of_components line 295
16. theorem OAI.Release075.TriangleFilling.active_reverse line 301
17. theorem OAI.Release075.TriangleFilling.active_next line 307
18. theorem OAI.Release075.TriangleFilling.active_of_mem line 313
19. theorem OAI.Release075.TriangleFilling.wedge line 319

    Source documentation

    Wedge two disks at their initial boundary corner. No component of either input that was disjoint from its boundary becomes an active component.

    theorem wedge {w w' : List E} (D : TriangleFilling flip color face w)
        (D' : TriangleFilling flip color face w')
        {a : D.Dart} {b : D'.Dart} {l : List D.Dart} {l' : List D'.Dart}
        (ha : D.boundary = a::l) (hb : D'.boundary = b::l')
        (hc : color (flip (D.label a)) = color (flip (D'.label b))) :
        Nonempty (TriangleFilling flip color face (w++w')) := by
    …

    Mentions: OAI.Release075.TriangleFilling

20. theorem OAI.Release075.PermCycles.dipoleReverse_involutive line 453
21. theorem OAI.Release075.PermCycles.dipoleReverse_ne line 456
22. theorem OAI.Release075.PermCycles.dipoleReverse_count line 459
23. theorem OAI.Release075.PermCycles.dipoleVertex_count line 466
24. theorem OAI.Release075.PermCycles.dipole_components line 477
25. theorem OAI.Release075.PermCycles.dipoleComponent_count line 500
26. theorem OAI.Release075.PermCycles.dipole_planar line 507
27. def OAI.Release075.TriangleFilling.triLabel line 518
28. def OAI.Release075.TriangleFilling.triangle line 522
29. theorem OAI.Release075.PermCycles.cycleCount_inv line 569
30. theorem OAI.Release075.PermCycles.components_inv_right line 574
31. theorem OAI.Release075.PermCycles.PlanarMap.inv_right line 579
32. theorem OAI.Release075.PermCycles.perm_apply_inv line 591
33. theorem OAI.Release075.PermCycles.inv_cycle_three line 594
34. theorem OAI.Release075.IsBoundary.reverse line 615
35. def OAI.Release075.TriangleFilling.mirror line 635

    Source documentation

    Reverse the orientation of the whole filling, not just its boundary word.

    noncomputable def mirror {w : List E} (D : TriangleFilling flip color face w)
        (hflip : Function.Involutive flip)
        (hface : ∀ a b c, face a b c → face (flip a) (flip c) (flip b)) :
        TriangleFilling flip color face (w.reverse.map flip) where
    …

    Mentions: OAI.Release075.TriangleFilling

36. def OAI.Release075.Fillable line 684

    Source documentation

    Existence of a finite labelled genus-zero filling. This abbreviation contains no geometric assertion outside the fully specified finite map.

    def Fillable (flip : E → E) (color : E → V) (face : E → E → E → Prop) (w : List E) : Prop :=
    …

37. theorem OAI.Release075.Fillable.empty line 689
38. theorem OAI.Release075.Fillable.rotateAppend line 691
39. theorem OAI.Release075.Fillable.mirror line 698
40. theorem OAI.Release075.Fillable.foldHead line 705
41. theorem OAI.Release075.Fillable.erase line 716
42. theorem OAI.Release075.Fillable.app line 723

    Source documentation

    Concatenate loops based at the same boundary corner. Empty words are allowed.

    theorem app {u v : List E} (hu : Fillable flip color face u) (hv : Fillable flip color face v)
        (hbase : ∀ e es f fs, u = e::es → v = f::fs →
          color (flip e) = color (flip f)) : Fillable flip color face (u++v) := by
    …

    Mentions: OAI.Release075.Fillable

43. theorem OAI.Release075.Fillable.backtrack line 740
44. theorem OAI.Release075.Fillable.stem line 744

    Source documentation

    Attach a stem, retaining its two directed traversals in the prescribed walk.

    theorem stem (hi : Function.Involutive flip) {w : List E}
        (h : Fillable flip color face w) (e : E)
        (hc : ∀ a l, w = a::l → color (flip a) = color e) :
        Fillable flip color face (e::w++[flip e]) := by
    …

    Mentions: OAI.Release075.Fillable