OAI/Combinatorics/StripMass/NodalTorusValue.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.mappedNodal_leading line 14
  2. lemma OAI.CriticalStrip.Diagram.mappedNodal_degree line 32
  3. lemma OAI.CriticalStrip.Diagram.lastValue_mul_poly line 39
  4. lemma OAI.CriticalStrip.Diagram.mappedNodal_pair_node line 46
  5. lemma OAI.CriticalStrip.Diagram.deletePoint_cosines line 81
  6. def OAI.CriticalStrip.Diagram.deleteEvaluation line 89
  7. lemma OAI.CriticalStrip.Diagram.deleteMapped_leading line 92
  8. lemma OAI.CriticalStrip.Diagram.deleteMapped_node line 104
  9. lemma OAI.CriticalStrip.Diagram.pairMapped_delete_leading line 128
  10. def OAI.CriticalStrip.Diagram.deletePairPolynomial line 143
  11. lemma OAI.CriticalStrip.Diagram.deletePairPolynomial_degree line 146
  12. lemma OAI.CriticalStrip.Diagram.deletePairPolynomial_top line 152
  13. lemma OAI.CriticalStrip.Diagram.deletePairPolynomial_eval line 159
  14. lemma OAI.CriticalStrip.Diagram.phase_four_ne_one line 169
  15. lemma OAI.CriticalStrip.Diagram.pairBeta_head_ne line 175
  16. lemma OAI.CriticalStrip.Diagram.pairBeta_injective line 186
  17. theorem OAI.CriticalStrip.Diagram.rationalNodalPolynomial_pair_delete line 207
  18. def OAI.CriticalStrip.Diagram.mergeZ line 266
  19. def OAI.CriticalStrip.Diagram.mergePoint line 267
  20. def OAI.CriticalStrip.Diagram.mergeNewWeights line 269
  21. def OAI.CriticalStrip.Diagram.mergeExponent line 272
  22. lemma OAI.CriticalStrip.Diagram.mergeNewWeights_phase line 274
  23. lemma OAI.CriticalStrip.Diagram.mergeExponent_le line 281
  24. lemma OAI.CriticalStrip.Diagram.mergeExponent_mixed line 284
  25. lemma OAI.CriticalStrip.Diagram.mergeNewWeights_regular line 293
  26. lemma OAI.CriticalStrip.Diagram.mergeZ_ne_zero line 297
  27. lemma OAI.CriticalStrip.Diagram.mergeZ_L line 298
  28. lemma OAI.CriticalStrip.Diagram.mergeZ_one_L line 300
  29. lemma OAI.CriticalStrip.Diagram.mergeZ_two_L line 303
  30. lemma OAI.CriticalStrip.Diagram.pairEarlier_merge line 307
  31. lemma OAI.CriticalStrip.Diagram.normalizedVacuum_pair_merge line 322
  32. lemma OAI.CriticalStrip.Diagram.mergePoint_ne_zero line 330
  33. lemma OAI.CriticalStrip.Diagram.mergePoint_weights line 335
  34. lemma OAI.CriticalStrip.Diagram.mergePoint_argument line 346
  35. lemma OAI.CriticalStrip.Diagram.mergePoint_L line 354
  36. lemma OAI.CriticalStrip.Diagram.mergePoint_cosines line 358
  37. def OAI.CriticalStrip.Diagram.mergeNodeWeights line 378
  38. lemma OAI.CriticalStrip.Diagram.mergeNode_regular line 381
  39. lemma OAI.CriticalStrip.Diagram.pairNode_merge line 404
  40. lemma OAI.CriticalStrip.Diagram.mergeNode_cons line 412
  41. lemma OAI.CriticalStrip.Diagram.normalizedVacuum_pairNode_merge line 419
  42. lemma OAI.CriticalStrip.Diagram.mergePoint_node_weights line 429
  43. lemma OAI.CriticalStrip.Diagram.mergePoint_node_L line 441
  44. def OAI.CriticalStrip.Diagram.mergeEvaluation line 459
  45. lemma OAI.CriticalStrip.Diagram.mergeMapped_leading line 462
  46. lemma OAI.CriticalStrip.Diagram.mergeMapped_node line 475
  47. lemma OAI.CriticalStrip.Diagram.pairMapped_merge_leading line 499
  48. def OAI.CriticalStrip.Diagram.mergePairPolynomial line 515
  49. lemma OAI.CriticalStrip.Diagram.mergePairPolynomial_degree line 518
  50. lemma OAI.CriticalStrip.Diagram.mergePairPolynomial_top line 522
  51. lemma OAI.CriticalStrip.Diagram.mergePairPolynomial_eval line 525