OAI/Combinatorics/StripMass/BlockPfaffian.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.blockFirst line 14
  2. def OAI.CriticalStrip.Diagram.blockSecond line 15
  3. theorem OAI.CriticalStrip.Diagram.blockFirst_injective line 17
  4. theorem OAI.CriticalStrip.Diagram.blockSecond_injective line 24
  5. theorem OAI.CriticalStrip.Diagram.blockFirst_ne_second line 31
  6. theorem OAI.CriticalStrip.Diagram.blockSecond_ne_first line 37
  7. theorem OAI.CriticalStrip.Diagram.blockFirst_zero line 40
  8. theorem OAI.CriticalStrip.Diagram.blockSecond_zero line 41
  9. def OAI.CriticalStrip.Diagram.blockSummand line 43
  10. def OAI.CriticalStrip.Diagram.blockSwap line 47
  11. theorem OAI.CriticalStrip.Diagram.blockSwap_first line 50
  12. theorem OAI.CriticalStrip.Diagram.blockSwap_second line 56
  13. theorem OAI.CriticalStrip.Diagram.blockSwap_sign line 63
  14. theorem OAI.CriticalStrip.Diagram.blockSummand_swap line 71
  15. def OAI.CriticalStrip.Diagram.blockFlip line 80
  16. theorem OAI.CriticalStrip.Diagram.blockFlip_first_zero line 82
  17. theorem OAI.CriticalStrip.Diagram.blockFlip_second_zero line 85
  18. theorem OAI.CriticalStrip.Diagram.blockFlip_first_succ line 88
  19. theorem OAI.CriticalStrip.Diagram.blockFlip_second_succ line 93
  20. theorem OAI.CriticalStrip.Diagram.blockFlip_sign line 98
  21. theorem OAI.CriticalStrip.Diagram.blockSummand_flip line 101
  22. def OAI.CriticalStrip.Diagram.blockSection line 114
  23. theorem OAI.CriticalStrip.Diagram.blockSection_zero line 118
  24. theorem OAI.CriticalStrip.Diagram.blockSummand_section line 131
  25. abbrev OAI.CriticalStrip.Diagram.FixedZero line 146
  26. instance OAI.CriticalStrip.Diagram.(instance at line 148) line 148
  27. def OAI.CriticalStrip.Diagram.fixedZeroEquiv line 150
  28. def OAI.CriticalStrip.Diagram.blockPermutationEquiv line 170
  29. theorem OAI.CriticalStrip.Diagram.blockSummand_section_inv line 194
  30. theorem OAI.CriticalStrip.Diagram.blockSummand_sum_fixedZero line 201
  31. theorem OAI.CriticalStrip.Diagram.blockFirst_succ line 217
  32. theorem OAI.CriticalStrip.Diagram.blockSecond_succ line 223
  33. theorem OAI.CriticalStrip.Diagram.blockSummand_fixTwo line 231
  34. theorem OAI.CriticalStrip.Diagram.blockSummand_isolated_zero line 257
  35. theorem OAI.CriticalStrip.Diagram.blockSummand_sum_isolated line 278
  36. theorem OAI.CriticalStrip.Diagram.pfaffian_eq_block line 309
  37. theorem OAI.CriticalStrip.Diagram.pfaffian_isolated line 326
  38. theorem OAI.CriticalStrip.Diagram.blockSummand_fixZero line 340
  39. theorem OAI.CriticalStrip.Diagram.pfaffian_firstRow_add line 364
  40. theorem OAI.CriticalStrip.Diagram.clearedPfaffianTerm_of_missing_pair line 398
  41. theorem OAI.CriticalStrip.Diagram.isolateFirstNumerator_prod_of_missing_pair line 409
  42. theorem OAI.CriticalStrip.Diagram.clearedPfaffian_collision line 440
  43. theorem OAI.CriticalStrip.Diagram.repairFirstDenominator_symm line 463
  44. theorem OAI.CriticalStrip.Diagram.isolateFirstNumerator_skew line 472
  45. theorem OAI.CriticalStrip.Diagram.clearedPfaffian_collision_formula line 486
  46. def OAI.CriticalStrip.Diagram.firstPairDecompose line 526
  47. theorem OAI.CriticalStrip.Diagram.prod_upperPair_succ line 551
  48. theorem OAI.CriticalStrip.Diagram.prod_upperPair_two line 562
  49. theorem OAI.CriticalStrip.Diagram.pfaffian_cast line 579
  50. theorem OAI.CriticalStrip.Diagram.clearedPfaffian_cast line 585
  51. theorem OAI.CriticalStrip.Diagram.clearedPfaffian_delete_even line 594