OAI/Combinatorics/StripMass/MirrorExterior.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.TriplePosition.mirrorInterface line 17
  2. def OAI.CriticalStrip.Diagram.TriplePosition.mirrorActive line 20
  3. def OAI.CriticalStrip.Diagram.TriplePosition.mirrorExterior line 24
  4. def OAI.CriticalStrip.Diagram.TriplePosition.MirrorOutside line 29
  5. def OAI.CriticalStrip.Diagram.TriplePosition.mirrorAttached line 32
  6. def OAI.CriticalStrip.Diagram.TriplePosition.mirrorPatch line 35
  7. def OAI.CriticalStrip.Diagram.TriplePosition.mirrorExteriorEquiv line 38
  8. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_boundary_old line 50
  9. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_boundary_new line 56
  10. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_interface_old line 63
  11. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_interface_new line 72
  12. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_exterior_edge line 88
  13. lemma OAI.CriticalStrip.Diagram.ThreeBox.reverseSlots_involutive line 126
  14. lemma OAI.CriticalStrip.Diagram.ThreeBox.reverseSlots_twice line 128
  15. def OAI.CriticalStrip.Diagram.ThreeBox.reverseEquiv line 130
  16. lemma OAI.CriticalStrip.Diagram.ThreeBox.support_mirror line 133
  17. lemma OAI.CriticalStrip.Diagram.ThreeBox.exterior_mirror line 140
  18. lemma OAI.CriticalStrip.Diagram.ThreeBox.exteriorTest_mirror line 162
  19. def OAI.CriticalStrip.Diagram.TriplePosition.mirrorExteriorPredicate line 189
  20. def OAI.CriticalStrip.Diagram.TriplePosition.mirrorPatchEquiv line 193
  21. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_active_iff line 198
  22. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_compatible_support_iff line 207
  23. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_patchTest_realizes line 232
  24. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_eval_patch_iff line 252
  25. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_eval_profile_iff line 273
  26. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_interface line 293
  27. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_active line 296
  28. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_exterior line 300
  29. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_outside line 307
  30. lemma OAI.CriticalStrip.Diagram.TriplePosition.mirror_predicate line 313
  31. def OAI.CriticalStrip.Diagram.tripleCircuit line 330
  32. def OAI.CriticalStrip.Diagram.tripleProgram line 333
  33. lemma OAI.CriticalStrip.Diagram.triple_expansion line 336
  34. def OAI.CriticalStrip.Diagram.ThreeBox.mirrorConfig line 351
  35. lemma OAI.CriticalStrip.Diagram.ThreeBox.config_sum_mirror line 354
  36. lemma OAI.CriticalStrip.Diagram.triple_expansion_mirror line 359
  37. theorem OAI.CriticalStrip.Diagram.TriplePosition.torus_yang_baxter line 385
  38. def OAI.CriticalStrip.Diagram.Position.Disjoint line 410
  39. lemma OAI.CriticalStrip.Diagram.Position.disjoint_symm line 413
  40. def OAI.CriticalStrip.Diagram.Position.pairCircuit line 416
  41. def OAI.CriticalStrip.Diagram.Position.exchangeEquiv line 419
  42. lemma OAI.CriticalStrip.Diagram.Position.exchange_edge line 431
  43. lemma OAI.CriticalStrip.Diagram.Position.exchange_boundary line 443
  44. lemma OAI.CriticalStrip.Diagram.Position.exchange_compatible line 452
  45. lemma OAI.CriticalStrip.Diagram.Position.exchange_eval line 459
  46. lemma OAI.CriticalStrip.Diagram.Position.steps_commute line 466
  47. lemma OAI.CriticalStrip.Diagram.localR_commute line 475
  48. lemma OAI.CriticalStrip.Diagram.Pairing.map_adj line 500
  49. lemma OAI.CriticalStrip.Diagram.Pairing.map_occupied line 511
  50. lemma OAI.CriticalStrip.Diagram.Pairing.map_partnerOrSelf line 522
  51. lemma OAI.CriticalStrip.Diagram.Pairing.map_cutShape line 530
  52. lemma OAI.CriticalStrip.Diagram.Pairing.map_cutLabels line 534
  53. lemma OAI.CriticalStrip.Diagram.Pairing.map_omit_adj line 538
  54. lemma OAI.CriticalStrip.Diagram.Pairing.map_cutRelation line 550
  55. lemma OAI.CriticalStrip.Diagram.Pairing.map_tileStep line 562