OAI/Combinatorics/StripMass/ArchRoots.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. abbrev OAI.CriticalStrip.Diagram.ArchShiftIndex line 13
  2. def OAI.CriticalStrip.Diagram.archRootShift line 15
  3. lemma OAI.CriticalStrip.Diagram.archRootShift_lt line 21
  4. lemma OAI.CriticalStrip.Diagram.archRootShift_injective line 25
  5. def OAI.CriticalStrip.Diagram.archRootCoefficient line 28
  6. lemma OAI.CriticalStrip.Diagram.archRootCoefficient_ne_zero line 31
  7. lemma OAI.CriticalStrip.Diagram.archRootCoefficient_injective line 35
  8. abbrev OAI.CriticalStrip.Diagram.ArchRootIndex line 47
  9. def OAI.CriticalStrip.Diagram.archRootExponent line 49
  10. def OAI.CriticalStrip.Diagram.archRootScalar line 53
  11. def OAI.CriticalStrip.Diagram.archRoot line 57
  12. lemma OAI.CriticalStrip.Diagram.archRootScalar_ne_zero line 60
  13. lemma OAI.CriticalStrip.Diagram.archRoot_ne_zero line 65
  14. lemma OAI.CriticalStrip.Diagram.archRootExponent_support line 72
  15. lemma OAI.CriticalStrip.Diagram.archRoot_injective line 76
  16. lemma OAI.CriticalStrip.Diagram.archRoot_none line 112
  17. lemma OAI.CriticalStrip.Diagram.archRoot_some line 115
  18. lemma OAI.CriticalStrip.Diagram.arch_pair_zero line 126
  19. lemma OAI.CriticalStrip.Diagram.arch_pair_zero_reverse line 138
  20. def OAI.CriticalStrip.Diagram.archEvaluate line 154
  21. lemma OAI.CriticalStrip.Diagram.archEvaluate_neg line 158
  22. lemma OAI.CriticalStrip.Diagram.archEvaluate_reflect line 166
  23. lemma OAI.CriticalStrip.Diagram.archEvaluate_pair line 175
  24. lemma OAI.CriticalStrip.Diagram.archShift_value line 190
  25. lemma OAI.CriticalStrip.Diagram.archEvaluate_shift line 199
  26. lemma OAI.CriticalStrip.Diagram.archEvaluate_roots line 224
  27. theorem OAI.CriticalStrip.Diagram.archLaurent_interpolation_zero line 245
  28. def OAI.CriticalStrip.Diagram.previousCoeff line 274
  29. lemma OAI.CriticalStrip.Diagram.previousCoeff_map line 277
  30. def OAI.CriticalStrip.Diagram.nextScalar line 283
  31. lemma OAI.CriticalStrip.Diagram.map_scalarValue line 286
  32. lemma OAI.CriticalStrip.Diagram.nextScalar_map line 291
  33. lemma OAI.CriticalStrip.Diagram.nextScalar_top line 296
  34. lemma OAI.CriticalStrip.Diagram.nextScalar_degree line 301
  35. def OAI.CriticalStrip.Diagram.headPerm line 306
  36. lemma OAI.CriticalStrip.Diagram.nextScalar_permute line 312
  37. def OAI.CriticalStrip.Diagram.scalarArchNumerator line 326
  38. lemma OAI.CriticalStrip.Diagram.map_scalarArchNumerator line 330
  39. lemma OAI.CriticalStrip.Diagram.scalarArchNumerator_permute line 336
  40. def OAI.CriticalStrip.Diagram.rowCosineL line 343
  41. lemma OAI.CriticalStrip.Diagram.rowCosineL_map line 346
  42. lemma OAI.CriticalStrip.Diagram.rowCosineL_algebraMap line 352
  43. lemma OAI.CriticalStrip.Diagram.rowCosineL_box line 355
  44. lemma OAI.CriticalStrip.Diagram.evalLaurent_constant_comp line 360
  45. lemma OAI.CriticalStrip.Diagram.scalarValue_rowCosine line 366
  46. lemma OAI.CriticalStrip.Diagram.nextScalar_rowCosine line 376
  47. def OAI.CriticalStrip.Diagram.archCandidate line 384
  48. lemma OAI.CriticalStrip.Diagram.archCandidate_eval line 386
  49. lemma OAI.CriticalStrip.Diagram.scalarValue_rowCosine_box line 392
  50. lemma OAI.CriticalStrip.Diagram.previousCoeff_nextScalar_box line 399
  51. lemma OAI.CriticalStrip.Diagram.archCandidate_box line 406
  52. lemma OAI.CriticalStrip.Diagram.archCandidate_permute line 422
  53. lemma OAI.CriticalStrip.Diagram.archCandidate_parity line 433
  54. lemma OAI.CriticalStrip.Diagram.archCandidate_row_reflection line 441
  55. lemma OAI.CriticalStrip.Diagram.previousCoeff_C_mul line 455
  56. lemma OAI.CriticalStrip.Diagram.previousCoeff_linear line 459
  57. lemma OAI.CriticalStrip.Diagram.previousCoeff_quadratic line 466
  58. lemma OAI.CriticalStrip.Diagram.specialization_constant_comp line 477
  59. lemma OAI.CriticalStrip.Diagram.torusEvaluation_rowCosine line 482
  60. lemma OAI.CriticalStrip.Diagram.firstFlatEvaluation_rowCosine line 491
  61. lemma OAI.CriticalStrip.Diagram.nextScalar_firstFlat line 498
  62. lemma OAI.CriticalStrip.Diagram.matrixPolynomial_merge_empty line 509
  63. lemma OAI.CriticalStrip.Diagram.matrixPolynomial_delete_empty line 515
  64. lemma OAI.CriticalStrip.Diagram.nextScalar_pair_merge line 521
  65. lemma OAI.CriticalStrip.Diagram.nextScalar_pair_delete line 533
  66. lemma OAI.CriticalStrip.Diagram.nextScalar_specialize line 545
  67. lemma OAI.CriticalStrip.Diagram.scalarValue_specialize line 551
  68. lemma OAI.CriticalStrip.Diagram.archCandidate_specialize line 558