OAI/Combinatorics/StripMass/ScalarMergeTrig.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. abbrev OAI.CriticalStrip.Diagram.fcos line 13
  2. lemma OAI.CriticalStrip.Diagram.fcos_eq line 15
  3. lemma OAI.CriticalStrip.Diagram.fcos_shift line 19
  4. lemma OAI.CriticalStrip.Diagram.fcos_eight line 25
  5. lemma OAI.CriticalStrip.Diagram.fcos_sub_eight line 31
  6. lemma OAI.CriticalStrip.Diagram.constF_d_sq line 36
  7. lemma OAI.CriticalStrip.Diagram.fcos_sum_product line 41
  8. lemma OAI.CriticalStrip.Diagram.fcos_six_ne line 61
  9. lemma OAI.CriticalStrip.Diagram.fcos_ne_const line 68
  10. lemma OAI.CriticalStrip.Diagram.scalar_merge_flat_constants line 82
  11. lemma OAI.CriticalStrip.Diagram.fcos_flat_factor line 94
  12. lemma OAI.CriticalStrip.Diagram.scalar_merge_delete_factor_algebra line 106
  13. lemma OAI.CriticalStrip.Diagram.fcos_sixteen line 118
  14. lemma OAI.CriticalStrip.Diagram.fcos_roots line 121
  15. lemma OAI.CriticalStrip.Diagram.roots_sum line 125
  16. lemma OAI.CriticalStrip.Diagram.fcos_delete_factor line 132
  17. lemma OAI.CriticalStrip.Diagram.scalarValue_fcos_delete line 155
  18. lemma OAI.CriticalStrip.Diagram.scalarMergeDiff_eval_neg line 166
  19. lemma OAI.CriticalStrip.Diagram.scalarMergeDiff_eval_flat line 178
  20. lemma OAI.CriticalStrip.Diagram.scalarMergeDiff_eval_deletion line 200
  21. lemma OAI.CriticalStrip.Diagram.fcos_tuple_injective line 237
  22. lemma OAI.CriticalStrip.Diagram.scalarMerge_nodes_injective line 243
  23. lemma OAI.CriticalStrip.Diagram.scalarValue_rotate3 line 263
  24. lemma OAI.CriticalStrip.Diagram.scalarValue_fcos_merge line 277
  25. lemma OAI.CriticalStrip.Diagram.rationalAt_scalarValue line 334
  26. lemma OAI.CriticalStrip.Diagram.rationalAt_copy_fcos line 341
  27. theorem OAI.CriticalStrip.Diagram.scalarValue_fcos_merge_all line 350
  28. lemma OAI.CriticalStrip.Diagram.torusEvaluation_lift line 392
  29. lemma OAI.CriticalStrip.Diagram.torusEvaluation_lastCosine line 404
  30. lemma OAI.CriticalStrip.Diagram.torusEvaluation_lastSine line 414
  31. lemma OAI.CriticalStrip.Diagram.torusEvaluation_lastLaurent line 421
  32. lemma OAI.CriticalStrip.Diagram.lastLaurent_regular_value line 445
  33. lemma OAI.CriticalStrip.Diagram.rationalAt_torusVacuum line 488
  34. lemma OAI.CriticalStrip.Diagram.torusEvaluation_vacuum line 512