OAI/GroupTheory/ArtinCAT0/Braids.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ArtinCAT0.BraidRelations line 13

    Source documentation

    The length-three and distant commutation relations on m successive letters. The letters are zero-indexed here.

    def BraidRelations (m : ℕ) (s : ℕ → G) : Prop :=
…
  2. def OAI.ArtinCAT0.braidLoop line 17
  3. def OAI.ArtinCAT0.braidCenter line 21
  4. def OAI.ArtinCAT0.braidDelta line 25
  5. lemma OAI.ArtinCAT0.commute_braidLoop line 29
  6. lemma OAI.ArtinCAT0.commute_braidCenter line 37
  7. lemma OAI.ArtinCAT0.commute_braidDelta line 44
  8. lemma OAI.ArtinCAT0.braid_loop_step line 51
  9. lemma OAI.ArtinCAT0.braidLoop_commute line 63
  10. lemma OAI.ArtinCAT0.braidLoops_commute line 77
  11. lemma OAI.ArtinCAT0.braid_center_step line 83
  12. lemma OAI.ArtinCAT0.braidCenter_commute line 91
  13. lemma OAI.ArtinCAT0.braidDelta_shift line 110
  14. lemma OAI.ArtinCAT0.braidDelta_conjugate line 132
  15. lemma OAI.ArtinCAT0.braid_conjugate line 138
  16. lemma OAI.ArtinCAT0.braidCenter_two line 142
  17. lemma OAI.ArtinCAT0.braidLoop_congr line 150
  18. lemma OAI.ArtinCAT0.braidCenter_congr line 157
  19. lemma OAI.ArtinCAT0.map_braidLoop line 164
  20. lemma OAI.ArtinCAT0.map_braidCenter line 170
  21. lemma OAI.ArtinCAT0.braidDelta_pow_conjugate line 176
  22. lemma OAI.ArtinCAT0.braidCenter_shift_conjugate line 190
  23. lemma OAI.ArtinCAT0.lengthPairing_braid_equal line 208
  24. lemma OAI.ArtinCAT0.lengthPairing_braid_constant line 218
  25. lemma OAI.ArtinCAT0.lengthPairing_braidLoop line 228
  26. lemma OAI.ArtinCAT0.lengthPairing_braidCenter line 243
  27. lemma OAI.ArtinCAT0.braidCenter_length_sq line 257
  28. lemma OAI.ArtinCAT0.braid_generator_length line 272
  29. lemma OAI.ArtinCAT0.braid_nonadjacent_pairing line 281
  30. lemma OAI.ArtinCAT0.lengthPairing_disjoint_centers line 302
  31. lemma OAI.ArtinCAT0.lengthPairing_braidDelta line 316
  32. lemma OAI.ArtinCAT0.equiangular_product_sq line 329
  33. lemma OAI.ArtinCAT0.braid_loop_character line 347
  34. lemma OAI.ArtinCAT0.braid_center_character line 364
  35. lemma OAI.ArtinCAT0.lengthPairing_le_self_of_equal_length line 380
  36. lemma OAI.ArtinCAT0.braid_forty_squared line 388

    Source documentation

    Quantitative braid constraint, in a division-free form.

    lemma braid_forty_squared (hG : GeometricAction G X) (x : X)
    {s : ℕ → G} (hs : BraidRelations 39 s) :
    143 * stableLengthAt x ((s 0)^2)^2 ≤ 57 * stableLengthAt x ((s 0*s 1)^3)^2 := by
…

    Mentions: OAI.ArtinCAT0.BraidRelations, OAI.ArtinCAT0.stableLengthAt

  37. lemma OAI.ArtinCAT0.braid_forty_ratio line 441
  38. abbrev OAI.ArtinCAT0.SelectedPositions line 462
  39. def OAI.ArtinCAT0.swapPositions line 464
  40. lemma OAI.ArtinCAT0.mem_swapPositions line 467
  41. lemma OAI.ArtinCAT0.card_swapPositions line 471
  42. lemma OAI.ArtinCAT0.swapPositions_twice line 474
  43. def OAI.ArtinCAT0.selectedPrefix line 479
  44. lemma OAI.ArtinCAT0.selectedPrefix_swap line 481
  45. lemma OAI.ArtinCAT0.selectedPrefix_succ line 493
  46. lemma OAI.ArtinCAT0.selectedPrefix_zero_of_three line 525
  47. lemma OAI.ArtinCAT0.selected_not_four line 538
  48. lemma OAI.ArtinCAT0.swapPositions_distant line 551
  49. lemma OAI.ArtinCAT0.swapPositions_braid line 573
  50. def OAI.ArtinCAT0.tokenRecord line 591
  51. lemma OAI.ArtinCAT0.tokenRecord_swap line 594
  52. abbrev OAI.ArtinCAT0.TokenState line 600
  53. def OAI.ArtinCAT0.tokenPerm line 602
  54. lemma OAI.ArtinCAT0.tokenRecord_distant line 610
  55. lemma OAI.ArtinCAT0.tokenPerm_distant line 623
  56. lemma OAI.ArtinCAT0.tokenPerm_braid line 642