OAI/Combinatorics/StripMass/BoundaryTree.lean

GitHub source file

82 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.FiniteBranchTree.leaves line 17
  2. def OAI.CriticalStrip.FiniteBranchTree.wordWeight line 27
  3. lemma OAI.CriticalStrip.FiniteBranchTree.wordWeight_nil line 31
  4. lemma OAI.CriticalStrip.FiniteBranchTree.wordWeight_cons line 32
  5. lemma OAI.CriticalStrip.FiniteBranchTree.prefix_disjoint line 35
  6. theorem OAI.CriticalStrip.FiniteBranchTree.mass_one line 44
  7. lemma OAI.CriticalStrip.FiniteBranchTree.nil_mem_iff line 58
  8. lemma OAI.CriticalStrip.FiniteBranchTree.cons_mem_iff line 63
  9. def OAI.CriticalStrip.FiniteBranchTree.visited line 73
  10. def OAI.CriticalStrip.FiniteBranchTree.terminal line 78
  11. lemma OAI.CriticalStrip.FiniteBranchTree.visited_length line 83
  12. lemma OAI.CriticalStrip.FiniteBranchTree.visited_mem_domain line 89
  13. lemma OAI.CriticalStrip.FiniteBranchTree.visited_nodup line 101
  14. lemma OAI.CriticalStrip.FiniteBranchTree.length_le_card line 113
  15. lemma OAI.CriticalStrip.FiniteBranchTree.terminal_append line 121
  16. lemma OAI.CriticalStrip.FiniteBranchTree.visited_append line 128
  17. lemma OAI.CriticalStrip.FiniteBranchTree.visited_head line 136
  18. lemma OAI.CriticalStrip.FiniteBranchTree.mem_leaves_iff line 144
  19. lemma OAI.CriticalStrip.FiniteBranchTree.terminal_outside_or_collision line 177
  20. lemma OAI.CriticalStrip.FiniteBranchTree.terminal_mem_domain_iff_collision line 195
  21. def OAI.CriticalStrip.FiniteBranchTree.exitMass line 202
  22. def OAI.CriticalStrip.FiniteBranchTree.collisionMass line 206
  23. theorem OAI.CriticalStrip.FiniteBranchTree.exit_add_collision line 212
  24. abbrev OAI.CriticalStrip.HoneycombBranch.Vertex line 234
  25. abbrev OAI.CriticalStrip.HoneycombBranch.State line 235
  26. def OAI.CriticalStrip.HoneycombBranch.neighbor line 237
  27. lemma OAI.CriticalStrip.HoneycombBranch.neighbor_reverse line 245
  28. lemma OAI.CriticalStrip.HoneycombBranch.neighbor_ne line 249
  29. lemma OAI.CriticalStrip.HoneycombBranch.neighbor_injective line 253
  30. def OAI.CriticalStrip.HoneycombBranch.outgoing line 260
  31. def OAI.CriticalStrip.HoneycombBranch.next line 262
  32. lemma OAI.CriticalStrip.HoneycombBranch.outgoing_ne line 266
  33. lemma OAI.CriticalStrip.HoneycombBranch.outgoing_injective line 269
  34. lemma OAI.CriticalStrip.HoneycombBranch.outgoing_exhaust line 273
  35. lemma OAI.CriticalStrip.HoneycombBranch.next_ne line 276
  36. lemma OAI.CriticalStrip.HoneycombBranch.next_back line 278
  37. lemma OAI.CriticalStrip.HoneycombBranch.next_not_back line 281
  38. lemma OAI.CriticalStrip.HoneycombBranch.next_injective line 284
  39. def OAI.CriticalStrip.HoneycombBranch.sign line 289
  40. def OAI.CriticalStrip.HoneycombBranch.turn line 291
  41. def OAI.CriticalStrip.HoneycombBranch.factor line 295
  42. lemma OAI.CriticalStrip.HoneycombBranch.factor_add line 297
  43. lemma OAI.CriticalStrip.HoneycombBranch.wordWeight_eq line 307
  44. lemma OAI.CriticalStrip.HoneycombBranch.phase_norm line 316
  45. lemma OAI.CriticalStrip.HoneycombBranch.wordWeight_norm line 319
  46. def OAI.CriticalStrip.HoneycombBranch.words line 324
  47. theorem OAI.CriticalStrip.HoneycombBranch.finite_tree_mass line 326
  48. theorem OAI.CriticalStrip.HoneycombBranch.exit_plus_collision line 331
  49. def OAI.CriticalStrip.HoneycombBranch.embedTriangle line 336
  50. lemma OAI.CriticalStrip.HoneycombBranch.embedTriangle_injective line 338
  51. lemma OAI.CriticalStrip.HoneycombBranch.adjacent_iff line 345
  52. lemma OAI.CriticalStrip.HoneycombBranch.visited_chain line 353
  53. def OAI.CriticalStrip.HoneycombBranch.direction line 366
  54. lemma OAI.CriticalStrip.HoneycombBranch.direction_next line 368
  55. lemma OAI.CriticalStrip.HoneycombBranch.direction_terminal line 373
  56. def OAI.CriticalStrip.HoneycombBranch.back line 388
  57. lemma OAI.CriticalStrip.HoneycombBranch.back_back line 390
  58. lemma OAI.CriticalStrip.HoneycombBranch.back_next line 393
  59. lemma OAI.CriticalStrip.HoneycombBranch.outgoing_opp line 397
  60. lemma OAI.CriticalStrip.HoneycombBranch.next_back_next line 400
  61. def OAI.CriticalStrip.HoneycombBranch.reverseTurns line 406
  62. lemma OAI.CriticalStrip.HoneycombBranch.reverseTurns_involutive line 408
  63. lemma OAI.CriticalStrip.HoneycombBranch.terminal_reverseTurns line 412
  64. lemma OAI.CriticalStrip.HoneycombBranch.visited_reverseTurns line 424
  65. lemma OAI.CriticalStrip.HoneycombBranch.turn_append line 438
  66. lemma OAI.CriticalStrip.HoneycombBranch.sign_not line 443
  67. lemma OAI.CriticalStrip.HoneycombBranch.turn_reverse line 445
  68. lemma OAI.CriticalStrip.HoneycombBranch.turn_map_not line 450
  69. lemma OAI.CriticalStrip.HoneycombBranch.turn_reverseTurns line 455
  70. def OAI.CriticalStrip.HoneycombBranch.reverseCycle line 460
  71. lemma OAI.CriticalStrip.HoneycombBranch.reverseCycle_involutive line 464
  72. lemma OAI.CriticalStrip.HoneycombBranch.reverseCycle_length line 469
  73. lemma OAI.CriticalStrip.HoneycombBranch.turn_reverseCycle line 472
  74. lemma OAI.CriticalStrip.HoneycombBranch.reverseCycle_ne line 477
  75. lemma OAI.CriticalStrip.HoneycombBranch.third_port line 482
  76. lemma OAI.CriticalStrip.HoneycombBranch.reverseCycle_first_step line 486
  77. lemma OAI.CriticalStrip.HoneycombBranch.terminal_reverseCycle line 495
  78. lemma OAI.CriticalStrip.HoneycombBranch.visited_reverseCycle line 503
  79. lemma OAI.CriticalStrip.HoneycombBranch.visited_reverseCycle_perm line 514
  80. lemma OAI.CriticalStrip.HoneycombBranch.prefix_reverseCycle_mem line 525
  81. lemma OAI.CriticalStrip.HoneycombBranch.phase_cancel line 547
  82. lemma OAI.CriticalStrip.HoneycombBranch.cycle_weight_cancel line 567