OAI/Combinatorics/StripMass/MergePairCandidate.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.rationalNodalPolynomial_pair_merge line 16
  2. lemma OAI.CriticalStrip.Diagram.torusEvaluation_fieldMap line 79
  3. def OAI.CriticalStrip.Diagram.freePoint line 90
  4. lemma OAI.CriticalStrip.Diagram.freePoint_ne_zero line 93
  5. lemma OAI.CriticalStrip.Diagram.freePoint_variable line 99
  6. lemma OAI.CriticalStrip.Diagram.freePoint_cons line 102
  7. lemma OAI.CriticalStrip.Diagram.torusEvaluation_free_lastLaurent line 110
  8. lemma OAI.CriticalStrip.Diagram.freePoint_firstFlat line 125
  9. lemma OAI.CriticalStrip.Diagram.freePoint_firstThree line 128
  10. lemma OAI.CriticalStrip.Diagram.freePoint_pair line 131
  11. lemma OAI.CriticalStrip.Diagram.firstFlatEvaluation_lastLaurent line 141
  12. lemma OAI.CriticalStrip.Diagram.firstThreeEvaluation_lastLaurent line 148
  13. lemma OAI.CriticalStrip.Diagram.lastValue_spectral line 161
  14. lemma OAI.CriticalStrip.Diagram.lastValue_C_mul line 166
  15. lemma OAI.CriticalStrip.Diagram.lastValue_firstZero_spectral line 173
  16. lemma OAI.CriticalStrip.Diagram.firstFlatCandidate_value line 204
  17. lemma OAI.CriticalStrip.Diagram.rationalVacuum_raw_stationary line 224
  18. lemma OAI.CriticalStrip.Diagram.residual_specialization_zero line 232
  19. theorem OAI.CriticalStrip.Diagram.residual_firstFlat line 250
  20. lemma OAI.CriticalStrip.Diagram.lastValue_mul_poly_map line 267
  21. lemma OAI.CriticalStrip.Diagram.firstThreeCandidate_value line 274
  22. theorem OAI.CriticalStrip.Diagram.residual_firstThree line 296
  23. lemma OAI.CriticalStrip.Diagram.torusEvaluation_unit_zpow line 317
  24. lemma OAI.CriticalStrip.Diagram.substitution_torusEvaluation_general line 322
  25. lemma OAI.CriticalStrip.Diagram.generic_substitution_zero line 338
  26. lemma OAI.CriticalStrip.Diagram.firstFlatEvaluation_zero_universal line 350
  27. lemma OAI.CriticalStrip.Diagram.firstThreeEvaluation_zero_universal line 359
  28. lemma OAI.CriticalStrip.Diagram.pairEvaluation_zero_universal line 368
  29. theorem OAI.CriticalStrip.Diagram.residual_flat_transport line 392
  30. def OAI.CriticalStrip.Diagram.PairExchangeRegular line 430
  31. lemma OAI.CriticalStrip.Diagram.PairExchangeRegular.perm line 434
  32. theorem OAI.CriticalStrip.Diagram.residual_pair_transport line 444
  33. def OAI.CriticalStrip.Diagram.fullPeel line 525
  34. lemma OAI.CriticalStrip.Diagram.fullPeel_injective line 528
  35. lemma OAI.CriticalStrip.Diagram.fullPeel_coeff line 531
  36. lemma OAI.CriticalStrip.Diagram.LaurentBox.fullPeel line 535
  37. lemma OAI.CriticalStrip.Diagram.fullPeel_monomial line 543
  38. lemma OAI.CriticalStrip.Diagram.evalLaurent_monomial_full line 551
  39. lemma OAI.CriticalStrip.Diagram.fullPeel_eval line 555