OAI/Combinatorics/StripMass/RibbonGlobal.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.HoneycombBranch.bottom line 18
  2. def OAI.CriticalStrip.HoneycombBranch.top line 19
  3. lemma OAI.CriticalStrip.HoneycombBranch.finite_columns line 21
  4. lemma OAI.CriticalStrip.HoneycombBranch.finite_rows line 41
  5. theorem OAI.CriticalStrip.HoneycombBranch.bottom_turn line 52
  6. lemma OAI.CriticalStrip.HoneycombBranch.closed_cycle_true_turn line 80
  7. theorem OAI.CriticalStrip.HoneycombBranch.collision_cycle_turn line 95
  8. theorem OAI.CriticalStrip.HoneycombBranch.collisionMass_zero line 142
  9. theorem OAI.CriticalStrip.HoneycombBranch.finite_boundary_flux line 155
  10. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.top_outside line 167
  11. lemma OAI.CriticalStrip.HoneycombBranch.RibbonRectangle.top_turn line 173
  12. theorem OAI.CriticalStrip.HoneycombBranch.top_turn line 207
  13. lemma OAI.CriticalStrip.HoneycombBranch.word_unique line 238
  14. lemma OAI.CriticalStrip.HoneycombBranch.exists_word line 266
  15. lemma OAI.CriticalStrip.HoneycombBranch.word_nonempty_of_head line 311
  16. lemma OAI.CriticalStrip.HoneycombBranch.word_terminal_ne_source line 319
  17. def OAI.CriticalStrip.HoneycombBranch.retractVertex line 337
  18. lemma OAI.CriticalStrip.HoneycombBranch.retract_embed line 339
  19. lemma OAI.CriticalStrip.HoneycombBranch.embed_retract line 342
  20. lemma OAI.CriticalStrip.HoneycombBranch.visited_head_last line 346
  21. lemma OAI.CriticalStrip.HoneycombBranch.visited_retract_path line 358
  22. lemma OAI.CriticalStrip.exists_column_to_bottom line 391
  23. lemma OAI.CriticalStrip.HoneycombBranch.terminal_eq_of_visited line 429
  24. def OAI.CriticalStrip.HoneycombBranch.SideWord line 441
  25. def OAI.CriticalStrip.HoneycombBranch.SideWord.state line 449
  26. def OAI.CriticalStrip.HoneycombBranch.SideWord.path line 451
  27. lemma OAI.CriticalStrip.HoneycombBranch.SideWord.band line 454
  28. lemma OAI.CriticalStrip.HoneycombBranch.SideWord.path_spec line 464
  29. lemma OAI.CriticalStrip.HoneycombBranch.SideWord.path_no_column line 472
  30. lemma OAI.CriticalStrip.HoneycombBranch.SideWord.connector_exists line 477
  31. def OAI.CriticalStrip.HoneycombBranch.SideWord.connector line 487
  32. lemma OAI.CriticalStrip.HoneycombBranch.SideWord.connector_spec line 488
  33. def OAI.CriticalStrip.HoneycombBranch.SideWord.arch line 492
  34. lemma OAI.CriticalStrip.HoneycombBranch.SideWord.arch_spec line 494
  35. lemma OAI.CriticalStrip.HoneycombBranch.SideWord.arch_filter line 504
  36. lemma OAI.CriticalStrip.HoneycombBranch.SideWord.path_embed line 512
  37. lemma OAI.CriticalStrip.HoneycombBranch.SideWord.arch_injective line 520
  38. lemma OAI.CriticalStrip.HoneycombBranch.SideWord.arch_length line 530
  39. lemma OAI.CriticalStrip.HoneycombBranch.SideWord.weighted_bound line 535
  40. lemma OAI.CriticalStrip.HoneycombBranch.SideWord.sum_le line 540