OAI/Combinatorics/StripMass/Specialization.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.RationalAt line 19
  2. theorem OAI.CriticalStrip.Diagram.RationalAt.algebraMap line 26
  3. theorem OAI.CriticalStrip.Diagram.RationalAt.zero line 30
  4. theorem OAI.CriticalStrip.Diagram.RationalAt.one line 34
  5. theorem OAI.CriticalStrip.Diagram.RationalAt.unique line 38
  6. theorem OAI.CriticalStrip.Diagram.RationalAt.add line 54
  7. theorem OAI.CriticalStrip.Diagram.RationalAt.mul line 63
  8. theorem OAI.CriticalStrip.Diagram.RationalAt.neg line 72
  9. theorem OAI.CriticalStrip.Diagram.RationalAt.sub line 77
  10. theorem OAI.CriticalStrip.Diagram.RationalAt.ne_zero line 81
  11. theorem OAI.CriticalStrip.Diagram.RationalAt.inv line 87
  12. theorem OAI.CriticalStrip.Diagram.RationalAt.div line 95
  13. theorem OAI.CriticalStrip.Diagram.RationalAt.pow line 100
  14. theorem OAI.CriticalStrip.Diagram.RationalAt.natCast line 106
  15. theorem OAI.CriticalStrip.Diagram.RationalAt.intCast line 110
  16. theorem OAI.CriticalStrip.Diagram.RationalAt.sum line 114
  17. theorem OAI.CriticalStrip.Diagram.RationalAt.prod line 125
  18. theorem OAI.CriticalStrip.Diagram.RationalAt.det line 149
  19. theorem OAI.CriticalStrip.Diagram.RationalAt.matrixOne line 159
  20. theorem OAI.CriticalStrip.Diagram.RationalAt.adjugate line 167
  21. theorem OAI.CriticalStrip.Diagram.RationalAt.nonsingInv line 184
  22. theorem OAI.CriticalStrip.Diagram.RationalAt.mulVec line 192
  23. theorem OAI.CriticalStrip.Diagram.rationalAt_column line 206
  24. theorem OAI.CriticalStrip.Diagram.rationalAt_normalizedVacuum line 220
  25. def OAI.CriticalStrip.Diagram.torusCharacter line 248
  26. def OAI.CriticalStrip.Diagram.torusEvaluation line 256
  27. theorem OAI.CriticalStrip.Diagram.torusEvaluation_monomial line 260
  28. theorem OAI.CriticalStrip.Diagram.torusEvaluation_constant line 265
  29. theorem OAI.CriticalStrip.Diagram.torusEvaluation_variable line 271
  30. theorem OAI.CriticalStrip.Diagram.rationalAt_const line 278
  31. theorem OAI.CriticalStrip.Diagram.rationalAt_variable line 285
  32. theorem OAI.CriticalStrip.Diagram.rationalAt_torusSin line 294
  33. theorem OAI.CriticalStrip.Diagram.rationalAt_torusCos line 306
  34. theorem OAI.CriticalStrip.Diagram.rationalAt_torusL line 312
  35. theorem OAI.CriticalStrip.Diagram.rationalAt_torusWeights line 321
  36. def OAI.CriticalStrip.Diagram.copiedNodeWeights line 355
  37. theorem OAI.CriticalStrip.Diagram.copiedNode_regular line 361
  38. def OAI.CriticalStrip.Diagram.copyEvaluation line 391
  39. lemma OAI.CriticalStrip.Diagram.rationalAt_copy_variable line 394
  40. lemma OAI.CriticalStrip.Diagram.rationalAt_copy_deletionNode line 398
  41. lemma OAI.CriticalStrip.Diagram.rationalAt_copy_spectralA line 402
  42. lemma OAI.CriticalStrip.Diagram.rationalAt_copy_deletionBeta line 409
  43. lemma OAI.CriticalStrip.Diagram.rationalAt_copy_weights line 417
  44. lemma OAI.CriticalStrip.Diagram.rationalAt_copy_vacuum line 438
  45. lemma OAI.CriticalStrip.Diagram.RationalAt.mv_eval line 450
  46. def OAI.CriticalStrip.Diagram.copiedNodeScalar line 461
  47. lemma OAI.CriticalStrip.Diagram.rationalAt_copy_scalar line 466
  48. lemma OAI.CriticalStrip.Diagram.rationalAt_copy_nodalVacuum line 475
  49. theorem OAI.CriticalStrip.Diagram.nodalVacuum_collision line 483
  50. theorem OAI.CriticalStrip.Diagram.occupied_nodal_collision line 493
  51. def OAI.CriticalStrip.Diagram.evalMonomialCharacter line 516
  52. lemma OAI.CriticalStrip.Diagram.evalLaurent_monomial_product line 525
  53. lemma OAI.CriticalStrip.Diagram.evalLaurent_unit_zpow line 538
  54. lemma OAI.CriticalStrip.Diagram.substituteLaurent_monomial line 542
  55. lemma OAI.CriticalStrip.Diagram.substitution_torusEvaluation line 549