OAI/Combinatorics/StripMass/GraphPath.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.PathGraph.AtMostTwo line 14
  2. def OAI.CriticalStrip.Diagram.PathGraph.AtMostOne line 17
  3. def OAI.CriticalStrip.Diagram.PathGraph.Trace line 21
  4. def OAI.CriticalStrip.Diagram.PathGraph.Consecutive line 25
  5. lemma OAI.CriticalStrip.Diagram.PathGraph.consecutive_symm line 29
  6. lemma OAI.CriticalStrip.Diagram.PathGraph.consecutive_mem line 34
  7. lemma OAI.CriticalStrip.Diagram.PathGraph.Trace.length_two_le line 40
  8. lemma OAI.CriticalStrip.Diagram.PathGraph.Trace.first line 48
  9. lemma OAI.CriticalStrip.Diagram.PathGraph.Trace.last line 53
  10. theorem OAI.CriticalStrip.Diagram.PathGraph.Trace.edge_consecutive line 60
  11. lemma OAI.CriticalStrip.Diagram.PathGraph.Trace.reach_mem line 97
  12. theorem OAI.CriticalStrip.Diagram.PathGraph.Trace.edges_iff line 111
  13. lemma OAI.CriticalStrip.Diagram.PathGraph.exists_trace line 126
  14. lemma OAI.CriticalStrip.Diagram.PathGraph.Trace.eq_singleton line 135
  15. lemma OAI.CriticalStrip.Diagram.PathGraph.Trace.avoid line 148
  16. theorem OAI.CriticalStrip.Diagram.PathGraph.Trace.unique line 159
  17. theorem OAI.CriticalStrip.Diagram.PathGraph.existsUnique_trace line 208
  18. lemma OAI.CriticalStrip.Diagram.PathGraph.consecutive_iff_neighbors line 215
  19. lemma OAI.CriticalStrip.Diagram.PathGraph.consecutive_irrefl line 233
  20. lemma OAI.CriticalStrip.Diagram.PathGraph.consecutive_two line 238
  21. lemma OAI.CriticalStrip.Diagram.PathGraph.consecutive_first_one line 247
  22. lemma OAI.CriticalStrip.Diagram.PathGraph.consecutive_last_one line 256
  23. lemma OAI.CriticalStrip.Diagram.PathGraph.consecutive_chain line 266
  24. lemma OAI.CriticalStrip.Diagram.PathGraph.Trace.used_of_mem line 271
  25. lemma OAI.CriticalStrip.Diagram.PathGraph.Trace.reach_of_mem line 283
  26. structure OAI.CriticalStrip.WireConfiguration line 306
  27. theorem OAI.CriticalStrip.WireConfiguration.ext line 319
  28. lemma OAI.CriticalStrip.WireConfiguration.reach line 322
  29. lemma OAI.CriticalStrip.WireConfiguration.existsUniqueTrace line 328
  30. def OAI.CriticalStrip.WireConfiguration.path line 334
  31. lemma OAI.CriticalStrip.WireConfiguration.path_trace line 337
  32. lemma OAI.CriticalStrip.WireConfiguration.path_isPath line 341
  33. lemma OAI.CriticalStrip.WireConfiguration.edges_iff line 349
  34. lemma OAI.CriticalStrip.WireConfiguration.support_eq line 354
  35. lemma OAI.CriticalStrip.WireConfiguration.support_finite line 363
  36. lemma OAI.CriticalStrip.WireConfiguration.support_ncard line 368
  37. def OAI.CriticalStrip.WireConfiguration.weight line 375
  38. lemma OAI.CriticalStrip.WireConfiguration.weight_eq line 377
  39. lemma OAI.CriticalStrip.WireConfiguration.ofPath_trace line 380
  40. def OAI.CriticalStrip.WireConfiguration.ofPath line 386
  41. lemma OAI.CriticalStrip.WireConfiguration.ofPath_graph line 406
  42. theorem OAI.CriticalStrip.WireConfiguration.ofPath_path line 410
  43. theorem OAI.CriticalStrip.WireConfiguration.ofPath_path_isPath line 415
  44. def OAI.CriticalStrip.WireConfiguration.equivPaths line 424
  45. lemma OAI.CriticalStrip.WireConfiguration.countable line 443
  46. lemma OAI.CriticalStrip.WireConfiguration.summable_weight_iff line 447
  47. lemma OAI.CriticalStrip.WireConfiguration.tsum_weight line 462
  48. theorem OAI.CriticalStrip.WireConfiguration.arch_sum line 474
  49. theorem OAI.CriticalStrip.WireConfiguration.arch_summable line 482
  50. theorem OAI.CriticalStrip.WireConfiguration.bridge_sum line 489
  51. theorem OAI.CriticalStrip.WireConfiguration.bridge_summable line 497
  52. lemma OAI.CriticalStrip.Diagram.PathGraph.Trace.two_neighbors line 516
  53. lemma OAI.CriticalStrip.WireConfiguration.another_neighbor line 540
  54. lemma OAI.CriticalStrip.adjacent_up_iff line 551
  55. lemma OAI.CriticalStrip.adjacent_down_iff line 559