OAI/Combinatorics/StripMass/SwapVacancy.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.Pairing.map_not_occupied_omit line 16
  2. lemma OAI.CriticalStrip.Diagram.Pairing.moveIntoVacancy_eq_self line 22
  3. lemma OAI.CriticalStrip.Diagram.Pairing.moveIntoVacancy_map_omit line 42
  4. lemma OAI.CriticalStrip.Diagram.localR_swap_vacant line 71
  5. lemma OAI.CriticalStrip.Diagram.localR_swap_omit line 89
  6. lemma OAI.CriticalStrip.Diagram.PartialColumn.insert_before_gate line 109
  7. lemma OAI.CriticalStrip.Diagram.PartialColumn.insert_after_gate line 127
  8. lemma OAI.CriticalStrip.Diagram.PartialColumn.insert_before_program line 145
  9. lemma OAI.CriticalStrip.Diagram.PartialColumn.insert_after_program line 163
  10. lemma OAI.CriticalStrip.Diagram.Pairing.map_map line 198
  11. lemma OAI.CriticalStrip.Diagram.Pairing.map_empty line 205
  12. lemma OAI.CriticalStrip.Diagram.Pairing.omit_padBottom line 209
  13. lemma OAI.CriticalStrip.Diagram.Pairing.omit_padTop line 220
  14. lemma OAI.CriticalStrip.Diagram.Pairing.omit_last line 231
  15. lemma OAI.CriticalStrip.Diagram.Pairing.omit_eq_padTop_exists line 237
  16. lemma OAI.CriticalStrip.Diagram.PartialColumn.program_column_all line 262
  17. lemma OAI.CriticalStrip.Diagram.PartialColumn.omit_top_matrix line 275
  18. theorem OAI.CriticalStrip.Diagram.PartialColumn.column_insert_swap line 296
  19. def OAI.CriticalStrip.Diagram.PartialColumn.twoRows line 322
  20. lemma OAI.CriticalStrip.Diagram.PartialColumn.twoRows₀ line 325
  21. lemma OAI.CriticalStrip.Diagram.PartialColumn.twoRows₁ line 327
  22. lemma OAI.CriticalStrip.Diagram.PartialColumn.twoRows_other line 329
  23. theorem OAI.CriticalStrip.Diagram.PartialColumn.column_merge_intertwiner line 334
  24. theorem OAI.CriticalStrip.Diagram.PartialColumn.column_deletion_intertwiner line 362
  25. lemma OAI.CriticalStrip.Diagram.Pairing.tileStep_empty_iff line 415
  26. lemma OAI.CriticalStrip.Diagram.localR_empty_row line 435
  27. lemma OAI.CriticalStrip.Diagram.localR_mulVec_empty line 443
  28. theorem OAI.CriticalStrip.Diagram.normalizedVacuum_torus_exchange line 449
  29. lemma OAI.CriticalStrip.Diagram.Pairing.map_eq_empty_iff line 473
  30. lemma OAI.CriticalStrip.Diagram.functionMatrix_map_mulVec_empty line 478
  31. def OAI.CriticalStrip.Diagram.mergeMap line 484
  32. def OAI.CriticalStrip.Diagram.deletionMap line 490
  33. lemma OAI.CriticalStrip.Diagram.mergeMap_mulVec_empty line 496
  34. lemma OAI.CriticalStrip.Diagram.deletionMap_mulVec_empty line 508
  35. theorem OAI.CriticalStrip.Diagram.normalizedVacuum_merge line 527
  36. theorem OAI.CriticalStrip.Diagram.normalizedVacuum_deletion line 548