OAI/Combinatorics/StripMass/PfaffianSupport.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.pfaffian_reindex line 16
  2. abbrev OAI.CriticalStrip.Diagram.UpperPair line 42
  3. instance OAI.CriticalStrip.Diagram.(instance at line 44) line 44
  4. def OAI.CriticalStrip.Diagram.upperPair line 47
  5. theorem OAI.CriticalStrip.Diagram.upperPair_symm line 50
  6. theorem OAI.CriticalStrip.Diagram.upperPair_eq_iff line 58
  7. theorem OAI.CriticalStrip.Diagram.pairFirst_ne_pairSecond line 63
  8. def OAI.CriticalStrip.Diagram.permutationPair line 70
  9. theorem OAI.CriticalStrip.Diagram.permutationPair_injective line 74
  10. theorem OAI.CriticalStrip.Diagram.upperPair_value line 91
  11. def OAI.CriticalStrip.Diagram.selectedPairs line 99
  12. def OAI.CriticalStrip.Diagram.clearedPfaffianTerm line 104
  13. def OAI.CriticalStrip.Diagram.clearedPfaffian line 109
  14. theorem OAI.CriticalStrip.Diagram.prod_selectedPairs line 113
  15. theorem OAI.CriticalStrip.Diagram.clearedPfaffianTerm_mul_denominator line 124
  16. theorem OAI.CriticalStrip.Diagram.clear_pfaffian line 134
  17. theorem OAI.CriticalStrip.Diagram.map_clearedPfaffianTerm line 157
  18. theorem OAI.CriticalStrip.Diagram.map_clearedPfaffian line 162
  19. def OAI.CriticalStrip.Diagram.augmentedNumerator line 175
  20. def OAI.CriticalStrip.Diagram.augmentedDenominator line 183
  21. theorem OAI.CriticalStrip.Diagram.discriminant_symm line 190
  22. theorem OAI.CriticalStrip.Diagram.augmentedDenominator_symm line 193
  23. theorem OAI.CriticalStrip.Diagram.augmentedKernel_eq line 200
  24. theorem OAI.CriticalStrip.Diagram.map_augmentedNumerator line 207
  25. theorem OAI.CriticalStrip.Diagram.map_augmentedDenominator line 214
  26. abbrev OAI.CriticalStrip.Diagram.CosineRing line 221
  27. abbrev OAI.CriticalStrip.Diagram.CosineField line 222
  28. def OAI.CriticalStrip.Diagram.cosineVar line 224
  29. def OAI.CriticalStrip.Diagram.cosineConst line 227
  30. def OAI.CriticalStrip.Diagram.scalarNumerator line 232
  31. theorem OAI.CriticalStrip.Diagram.discriminant_cosineVar_ne line 238
  32. theorem OAI.CriticalStrip.Diagram.augmentedDenominator_cosineVar_ne line 255
  33. theorem OAI.CriticalStrip.Diagram.scalarNumerator_generic line 262
  34. def OAI.CriticalStrip.Diagram.upperPairMap line 289
  35. theorem OAI.CriticalStrip.Diagram.upperPairMap_injective line 292
  36. def OAI.CriticalStrip.Diagram.upperPairPerm line 304
  37. theorem OAI.CriticalStrip.Diagram.prod_upperPair_reindex line 309
  38. theorem OAI.CriticalStrip.Diagram.prod_upperPair line 317
  39. def OAI.CriticalStrip.Diagram.upperPairEmbed line 330
  40. theorem OAI.CriticalStrip.Diagram.upperPairEmbed_injective line 333
  41. theorem OAI.CriticalStrip.Diagram.scalarNumerator_eval line 350
  42. theorem OAI.CriticalStrip.Diagram.product_augmentedDenominator line 371
  43. theorem OAI.CriticalStrip.Diagram.scalarNumerator_eval_vandermonde line 394
  44. def OAI.CriticalStrip.Diagram.augmentedPerm line 415
  45. theorem OAI.CriticalStrip.Diagram.augmentedPerm_real line 418
  46. theorem OAI.CriticalStrip.Diagram.augmentedPerm_extra line 422
  47. theorem OAI.CriticalStrip.Diagram.augmentedPerm_apply line 430
  48. theorem OAI.CriticalStrip.Diagram.augmentedPerm_sign line 436
  49. theorem OAI.CriticalStrip.Diagram.augmentedNumerator_reindex line 443
  50. theorem OAI.CriticalStrip.Diagram.augmentedDenominator_reindex line 451
  51. theorem OAI.CriticalStrip.Diagram.augmentedKernel_reindex line 459
  52. theorem OAI.CriticalStrip.Diagram.scalarNumerator_eval_reindex line 469
  53. def OAI.CriticalStrip.Diagram.cosineCoeff line 484
  54. theorem OAI.CriticalStrip.Diagram.cosineCoeff_apply line 487
  55. theorem OAI.CriticalStrip.Diagram.eval₂_cosineCoeff line 489
  56. theorem OAI.CriticalStrip.Diagram.scalarNumerator_rename line 496