OAI/Combinatorics/StripMass/PairSelfNode.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.matrixPrefix_zero_of_first line 15
  2. lemma OAI.CriticalStrip.Diagram.reducedMovingStepL_pair_zero line 22
  3. lemma OAI.CriticalStrip.Diagram.nodalDatumL_pair_self_zero line 31
  4. lemma OAI.CriticalStrip.Diagram.rationalNodalPolynomial_laurent_at_node line 45
  5. theorem OAI.CriticalStrip.Diagram.rationalNodalPolynomial_pair_self line 67
  6. def OAI.CriticalStrip.Diagram.pairIndex line 83
  7. def OAI.CriticalStrip.Diagram.pairExponent line 84
  8. def OAI.CriticalStrip.Diagram.pairEarlierWeights line 86
  9. def OAI.CriticalStrip.Diagram.pairNodeWeights line 89
  10. lemma OAI.CriticalStrip.Diagram.pairExponent_le line 92
  11. lemma OAI.CriticalStrip.Diagram.pairExponent_mixed line 95
  12. lemma OAI.CriticalStrip.Diagram.pairEarlier_regular line 102
  13. lemma OAI.CriticalStrip.Diagram.pairNode_regular line 105
  14. lemma OAI.CriticalStrip.Diagram.pairPoint_of_ne line 119
  15. lemma OAI.CriticalStrip.Diagram.pairArgument line 127
  16. lemma OAI.CriticalStrip.Diagram.pairEarlier_L line 139
  17. lemma OAI.CriticalStrip.Diagram.rationalAt_pair_nodalWeights line 144
  18. lemma OAI.CriticalStrip.Diagram.phaseCosine line 168
  19. def OAI.CriticalStrip.Diagram.pairCosines line 175
  20. def OAI.CriticalStrip.Diagram.pairBeta line 177
  21. lemma OAI.CriticalStrip.Diagram.pairPoint_cosine line 180
  22. lemma OAI.CriticalStrip.Diagram.pairNode_cosine line 188
  23. lemma OAI.CriticalStrip.Diagram.rationalAt_pair_spectralA line 202
  24. lemma OAI.CriticalStrip.Diagram.rationalAt_pair_deletionNode line 209
  25. lemma OAI.CriticalStrip.Diagram.rationalAt_pair_deletionBeta line 214
  26. lemma OAI.CriticalStrip.Diagram.pairEvaluation_betaL line 222
  27. lemma OAI.CriticalStrip.Diagram.pairBeta_of_ne line 229
  28. lemma OAI.CriticalStrip.Diagram.rationalAt_pair_nodalScalar line 233
  29. lemma OAI.CriticalStrip.Diagram.rationalAt_pair_nodalVacuum line 242
  30. lemma OAI.CriticalStrip.Diagram.twoRows_omit_one line 255
  31. lemma OAI.CriticalStrip.Diagram.omit_first_two line 263
  32. lemma OAI.CriticalStrip.Diagram.normalizedVacuum_merge_cons line 269
  33. lemma OAI.CriticalStrip.Diagram.normalizedVacuum_deletion_cons line 288
  34. def OAI.CriticalStrip.Diagram.deletePoint line 309
  35. def OAI.CriticalStrip.Diagram.deleteWeights line 311
  36. lemma OAI.CriticalStrip.Diagram.deleteWeights_regular line 314
  37. lemma OAI.CriticalStrip.Diagram.pairEarlier_delete line 317
  38. lemma OAI.CriticalStrip.Diagram.normalizedVacuum_pair_delete line 329
  39. lemma OAI.CriticalStrip.Diagram.pairNode_delete line 339
  40. lemma OAI.CriticalStrip.Diagram.normalizedVacuum_pairNode_delete line 347
  41. lemma OAI.CriticalStrip.Diagram.deletePoint_node_weights line 358
  42. lemma OAI.CriticalStrip.Diagram.deletePoint_node_L line 371
  43. lemma OAI.CriticalStrip.Diagram.Fin.snoc_twoCons line 389
  44. def OAI.CriticalStrip.Diagram.deletePairScalar line 393
  45. def OAI.CriticalStrip.Diagram.mergePairScalar line 397
  46. lemma OAI.CriticalStrip.Diagram.scalar_pair_delete line 400
  47. lemma OAI.CriticalStrip.Diagram.scalar_pair_delete_snoc line 405
  48. lemma OAI.CriticalStrip.Diagram.scalar_pair_merge line 419
  49. lemma OAI.CriticalStrip.Diagram.scalar_pair_merge_snoc line 425
  50. lemma OAI.CriticalStrip.Diagram.mergeMap_last line 457
  51. lemma OAI.CriticalStrip.Diagram.mergeMap_padTop line 464
  52. lemma OAI.CriticalStrip.Diagram.deletionMap_last line 475
  53. lemma OAI.CriticalStrip.Diagram.deletionMap_padTop line 484
  54. lemma OAI.CriticalStrip.Diagram.LastDegree.mul_poly line 507
  55. lemma OAI.CriticalStrip.Diagram.LastDegree.mul_poly_top line 519