OAI/Combinatorics/StripMass/CutPatch.lean

GitHub source file

58 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. inductive OAI.CriticalStrip.Diagram.CutPatch.Shape line 15
  2. instance OAI.CriticalStrip.Diagram.CutPatch.(instance at line 19) line 19
  3. def OAI.CriticalStrip.Diagram.CutPatch.inputEdges line 21
  4. def OAI.CriticalStrip.Diagram.CutPatch.tilePort line 28
  5. def OAI.CriticalStrip.Diagram.CutPatch.Adj line 30
  6. instance OAI.CriticalStrip.Diagram.CutPatch.(instance at line 34) line 34
  7. def OAI.CriticalStrip.Diagram.CutPatch.inputOccupied line 37
  8. instance OAI.CriticalStrip.Diagram.CutPatch.(instance at line 41) line 41
  9. def OAI.CriticalStrip.Diagram.CutPatch.Compatible line 44
  10. instance OAI.CriticalStrip.Diagram.CutPatch.(instance at line 47) line 47
  11. def OAI.CriticalStrip.Diagram.CutPatch.boundary line 50
  12. def OAI.CriticalStrip.Diagram.CutPatch.active line 52
  13. instance OAI.CriticalStrip.Diagram.CutPatch.(instance at line 55) line 55
  14. def OAI.CriticalStrip.Diagram.CutPatch.boundaryAdj line 58
  15. def OAI.CriticalStrip.Diagram.CutPatch.boundarySupport line 61
  16. instance OAI.CriticalStrip.Diagram.CutPatch.(instance at line 64) line 64
  17. instance OAI.CriticalStrip.Diagram.CutPatch.(instance at line 66) line 66
  18. def OAI.CriticalStrip.Diagram.CutPatch.profile line 69
  19. def OAI.CriticalStrip.Diagram.CutPatch.rootTable line 82
  20. def OAI.CriticalStrip.Diagram.CutPatch.parentTable line 129
  21. def OAI.CriticalStrip.Diagram.CutPatch.rankTable line 176
  22. def OAI.CriticalStrip.Diagram.CutPatch.ForestConditions line 223
  23. instance OAI.CriticalStrip.Diagram.CutPatch.(instance at line 228) line 228
  24. theorem OAI.CriticalStrip.Diagram.CutPatch.forestConditions line 231
  25. def OAI.CriticalStrip.Diagram.CutPatch.forest line 234
  26. theorem OAI.CriticalStrip.Diagram.CutPatch.adj_symmetric line 242
  27. theorem OAI.CriticalStrip.Diagram.CutPatch.reach_iff line 250
  28. def OAI.CriticalStrip.Diagram.CutPatch.GoodChecks line 254
  29. def OAI.CriticalStrip.Diagram.CutPatch.BadChecks line 259
  30. instance OAI.CriticalStrip.Diagram.CutPatch.(instance at line 263) line 263
  31. instance OAI.CriticalStrip.Diagram.CutPatch.(instance at line 265) line 265
  32. def OAI.CriticalStrip.Diagram.CutPatch.ProfileChecks line 268
  33. instance OAI.CriticalStrip.Diagram.CutPatch.(instance at line 273) line 273
  34. theorem OAI.CriticalStrip.Diagram.CutPatch.profileChecks line 276
  35. structure OAI.CriticalStrip.Diagram.CutPatch.Realizes line 279
  36. theorem OAI.CriticalStrip.Diagram.CutPatch.realizes_of_profile line 285
  37. theorem OAI.CriticalStrip.Diagram.CutPatch.none_has_closed line 294
  38. def OAI.CriticalStrip.Diagram.Pairing.partnerOrSelf line 316
  39. theorem OAI.CriticalStrip.Diagram.Pairing.adj_partnerOrSelf line 319
  40. theorem OAI.CriticalStrip.Diagram.Pairing.adj_omit_decomposition line 327
  41. theorem OAI.CriticalStrip.Diagram.Pairing.insertCup_adj line 350
  42. theorem OAI.CriticalStrip.Diagram.Pairing.mapOccupied_equiv_adj line 358
  43. theorem OAI.CriticalStrip.Diagram.Pairing.moveIntoVacancy_adj line 365
  44. theorem OAI.CriticalStrip.Diagram.Pairing.moveIntoLowerVacancy_adj line 371
  45. theorem OAI.CriticalStrip.Diagram.Pairing.capRemove_adj line 377
  46. def OAI.CriticalStrip.Diagram.Pairing.cutShape line 386
  47. def OAI.CriticalStrip.Diagram.Pairing.cutLabels line 392
  48. theorem OAI.CriticalStrip.Diagram.Pairing.tileStep_none_iff line 395
  49. theorem OAI.CriticalStrip.Diagram.Pairing.adj_decompose_partners line 407
  50. theorem OAI.CriticalStrip.Diagram.Pairing.omitTwo_swap_invariant line 415
  51. theorem OAI.CriticalStrip.Diagram.Pairing.partnerOrSelf_ne line 422
  52. theorem OAI.CriticalStrip.Diagram.Pairing.partnerOrSelf_ne_of_vacant line 429
  53. theorem OAI.CriticalStrip.Diagram.Pairing.swap_eq_partner_iff line 436
  54. theorem OAI.CriticalStrip.Diagram.Pairing.swap_eq_partner_iff_lower line 444
  55. def OAI.CriticalStrip.Diagram.Pairing.cutRelation line 452
  56. theorem OAI.CriticalStrip.Diagram.Pairing.cutRelation_empty line 457
  57. theorem OAI.CriticalStrip.Diagram.Pairing.cutRelation_single line 461
  58. theorem OAI.CriticalStrip.Diagram.Pairing.cutRelation_union line 476