OAI/Combinatorics/StripMass/CollisionSubstitutions.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.cosineCollisionPacket_eval_root line 15
  2. def OAI.CriticalStrip.Diagram.collisionCopy line 29
  3. def OAI.CriticalStrip.Diagram.collisionSubstitution line 31
  4. lemma OAI.CriticalStrip.Diagram.collisionSubstitution_beta_self line 36
  5. lemma OAI.CriticalStrip.Diagram.collisionSubstitution_beta line 54
  6. lemma OAI.CriticalStrip.Diagram.collisionCopy_eq line 62
  7. lemma OAI.CriticalStrip.Diagram.collisionSubstitution_cross line 81
  8. lemma OAI.CriticalStrip.Diagram.copyEvaluation_collision line 104
  9. lemma OAI.CriticalStrip.Diagram.nodalDatumL_copy_collision line 112
  10. lemma OAI.CriticalStrip.Diagram.nodalDatumL_ordinary_collision line 136
  11. def OAI.CriticalStrip.Diagram.reflectionUnit line 150
  12. lemma OAI.CriticalStrip.Diagram.reflectionUnit_coe line 153
  13. lemma OAI.CriticalStrip.Diagram.reflectionUnit_inv_coe line 158
  14. lemma OAI.CriticalStrip.Diagram.substitute_reflection_sine line 163
  15. lemma OAI.CriticalStrip.Diagram.reflectionFactorL_collision_left line 187
  16. lemma OAI.CriticalStrip.Diagram.reflectionFactorL_collision_right line 192
  17. lemma OAI.CriticalStrip.Diagram.nodalDatumL_reflection line 198
  18. lemma OAI.CriticalStrip.Diagram.substituteLaurent_neg_sign_monomial line 214
  19. lemma OAI.CriticalStrip.Diagram.substituteLaurent_neg_sign line 227
  20. lemma OAI.CriticalStrip.Diagram.nodalDatumL_collision line 243
  21. lemma OAI.CriticalStrip.Diagram.interpolationNumerator_collisionSubstitution line 262
  22. def OAI.CriticalStrip.Diagram.upperPairOther line 279
  23. lemma OAI.CriticalStrip.Diagram.upperPairOther_spec line 282
  24. def OAI.CriticalStrip.Diagram.edgeSubstitution line 286
  25. lemma OAI.CriticalStrip.Diagram.edgeSubstitution_kernel line 289
  26. lemma OAI.CriticalStrip.Diagram.edgeSubstitution_cross line 297
  27. theorem OAI.CriticalStrip.Diagram.nodal_vandermonde_dvd line 313
  28. lemma OAI.CriticalStrip.Diagram.interpolate_lift_of_vandermonde_dvd line 334
  29. lemma OAI.CriticalStrip.Diagram.nodalLow_laurent line 364
  30. lemma OAI.CriticalStrip.Diagram.rationalNodalPolynomial_laurent line 379
  31. def OAI.CriticalStrip.Diagram.PolynomialBox line 405
  32. lemma OAI.CriticalStrip.Diagram.PolynomialBox.mono line 408
  33. lemma OAI.CriticalStrip.Diagram.PolynomialBox.zero line 410
  34. lemma OAI.CriticalStrip.Diagram.PolynomialBox.C line 414
  35. lemma OAI.CriticalStrip.Diagram.PolynomialBox.X line 421
  36. lemma OAI.CriticalStrip.Diagram.PolynomialBox.add line 427
  37. lemma OAI.CriticalStrip.Diagram.PolynomialBox.sub line 430
  38. lemma OAI.CriticalStrip.Diagram.PolynomialBox.mul line 433
  39. lemma OAI.CriticalStrip.Diagram.PolynomialBox.one line 438
  40. lemma OAI.CriticalStrip.Diagram.PolynomialBox.prod line 440
  41. lemma OAI.CriticalStrip.Diagram.nodalLow_laurent_box line 458
  42. lemma OAI.CriticalStrip.Diagram.nodal_betaL_box line 521
  43. lemma OAI.CriticalStrip.Diagram.rationalNodalPolynomial_laurent_box line 532