OAI/Combinatorics/StripMass/AugmentedTail.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.twoCons line 14
  2. theorem OAI.CriticalStrip.Diagram.twoCons_zero line 17
  3. theorem OAI.CriticalStrip.Diagram.twoCons_one line 20
  4. theorem OAI.CriticalStrip.Diagram.twoCons_succ_succ line 25
  5. theorem OAI.CriticalStrip.Diagram.twoCons_of_ge line 28
  6. def OAI.CriticalStrip.Diagram.augmentTwoIndex line 40
  7. theorem OAI.CriticalStrip.Diagram.augmentTwoIndex_val line 43
  8. theorem OAI.CriticalStrip.Diagram.augmentTwoIndex_zero line 46
  9. theorem OAI.CriticalStrip.Diagram.augmentTwoIndex_one line 50
  10. theorem OAI.CriticalStrip.Diagram.augmentedNumerator_skew line 54
  11. theorem OAI.CriticalStrip.Diagram.augmentedNumerator_two_zero_one line 61
  12. theorem OAI.CriticalStrip.Diagram.augmentedDenominator_two_zero_one line 66
  13. theorem OAI.CriticalStrip.Diagram.augmentedNumerator_two_tail line 71
  14. theorem OAI.CriticalStrip.Diagram.augmentedDenominator_two_tail line 80
  15. theorem OAI.CriticalStrip.Diagram.prod_pad_one line 90
  16. theorem OAI.CriticalStrip.Diagram.augmentedDenominator_two_zero_tail line 104
  17. theorem OAI.CriticalStrip.Diagram.augmentedDenominator_two_one_tail line 113
  18. theorem OAI.CriticalStrip.Diagram.augmentedDenominator_two_cross line 125
  19. theorem OAI.CriticalStrip.Diagram.scalarNumerator_eval_cleared line 151
  20. theorem OAI.CriticalStrip.Diagram.scalarNumerator_delete line 160
  21. theorem OAI.CriticalStrip.Diagram.sourceVandermonde_twoCons line 233
  22. theorem OAI.CriticalStrip.Diagram.scalarPolynomial_delete_mul line 243
  23. theorem OAI.CriticalStrip.Diagram.scalarPolynomial_delete_roots line 267
  24. theorem OAI.CriticalStrip.Diagram.cos_six_lambda line 315
  25. theorem OAI.CriticalStrip.Diagram.sin_six_lambda line 320
  26. theorem OAI.CriticalStrip.Diagram.d_sq line 326
  27. theorem OAI.CriticalStrip.Diagram.d_ne_zero line 332
  28. theorem OAI.CriticalStrip.Diagram.discriminant_cosine_roots line 339
  29. theorem OAI.CriticalStrip.Diagram.discriminant_cosine_roots_complex line 348
  30. theorem OAI.CriticalStrip.Diagram.scalarPolynomial_delete_cosine line 367
  31. def OAI.CriticalStrip.Diagram.LastDegree line 396
  32. theorem OAI.CriticalStrip.Diagram.lastTransform_coeff_succ line 400
  33. theorem OAI.CriticalStrip.Diagram.lastTransform_degree line 417
  34. theorem OAI.CriticalStrip.Diagram.Pairing.padTop_injective line 440
  35. theorem OAI.CriticalStrip.Diagram.lastTransform_leading line 447
  36. def OAI.CriticalStrip.Diagram.deletionNode line 481
  37. def OAI.CriticalStrip.Diagram.deletionBeta line 484
  38. def OAI.CriticalStrip.Diagram.nodalWeights line 487
  39. def OAI.CriticalStrip.Diagram.nodalScalar line 492
  40. def OAI.CriticalStrip.Diagram.nodalVacuum line 497
  41. def OAI.CriticalStrip.Diagram.rationalVacuum line 502
  42. def OAI.CriticalStrip.Diagram.rationalNodalPolynomial line 507
  43. def OAI.CriticalStrip.Diagram.rationalInterpolant line 518
  44. def OAI.CriticalStrip.Diagram.rationalInterpolationResidual line 524