OAI/Combinatorics/StripMass/FirstThree.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. lemma OAI.CriticalStrip.Diagram.vacantBottomExtension_smul line 14
  2. lemma OAI.CriticalStrip.Diagram.normalizedVacuum_firstThree line 20
  3. def OAI.CriticalStrip.Diagram.firstThreePoint line 43
  4. lemma OAI.CriticalStrip.Diagram.firstThreePoint_ne_zero line 46
  5. def OAI.CriticalStrip.Diagram.firstThreeEvaluation line 51
  6. lemma OAI.CriticalStrip.Diagram.rationalAt_firstThree_variable line 54
  7. lemma OAI.CriticalStrip.Diagram.rationalAt_firstThree_spectralA line 58
  8. lemma OAI.CriticalStrip.Diagram.rationalAt_firstThree_deletionNode line 74
  9. lemma OAI.CriticalStrip.Diagram.firstThreeNode_ne_zero line 83
  10. lemma OAI.CriticalStrip.Diagram.torusCos_phase_nine line 89
  11. lemma OAI.CriticalStrip.Diagram.rationalAt_firstThree_deletionBeta line 94
  12. lemma OAI.CriticalStrip.Diagram.rationalAt_firstThree_weights line 110
  13. lemma OAI.CriticalStrip.Diagram.rationalAt_firstThree_normalization line 129
  14. lemma OAI.CriticalStrip.Diagram.rationalAt_firstThree_vacuum line 140
  15. lemma OAI.CriticalStrip.Diagram.firstThreeHead_zero line 160
  16. lemma OAI.CriticalStrip.Diagram.nodalDatumL_firstThree_zero line 190
  17. lemma OAI.CriticalStrip.Diagram.rationalNodalPolynomial_firstThree_self line 194
  18. lemma OAI.CriticalStrip.Diagram.rationalAt_firstThree_nodalWeights line 228
  19. lemma OAI.CriticalStrip.Diagram.rationalAt_firstThree_nodalScalar line 251
  20. lemma OAI.CriticalStrip.Diagram.rationalAt_firstThree_nodalVacuum line 270
  21. def OAI.CriticalStrip.Diagram.firstThreePolynomial line 291
  22. lemma OAI.CriticalStrip.Diagram.firstThreePolynomial_padBottom line 295
  23. lemma OAI.CriticalStrip.Diagram.firstThreePolynomial_degree line 300
  24. lemma OAI.CriticalStrip.Diagram.firstThreePolynomial_leading line 318
  25. lemma OAI.CriticalStrip.Diagram.firstThreeBeta_injective line 331
  26. theorem OAI.CriticalStrip.Diagram.rationalNodalPolynomial_firstThree line 341
  27. lemma OAI.CriticalStrip.Diagram.vacuumRegular_of_rationalAt line 414
  28. lemma OAI.CriticalStrip.Diagram.torusRegular_of_rationalAt line 424
  29. def OAI.CriticalStrip.Diagram.pairPoint line 434
  30. lemma OAI.CriticalStrip.Diagram.pairPoint_ne_zero line 436
  31. def OAI.CriticalStrip.Diagram.pairEvaluation line 443
  32. lemma OAI.CriticalStrip.Diagram.rationalAt_pair_variable line 446
  33. lemma OAI.CriticalStrip.Diagram.torusL_phase_five line 450
  34. lemma OAI.CriticalStrip.Diagram.torusL_phase_six line 457
  35. lemma OAI.CriticalStrip.Diagram.pairEvaluation_vacantNumerator line 464
  36. lemma OAI.CriticalStrip.Diagram.torusL_phase_small_ne_zero line 492
  37. def OAI.CriticalStrip.Diagram.allOneEvaluation line 501
  38. lemma OAI.CriticalStrip.Diagram.rationalAt_phaseRow line 504
  39. lemma OAI.CriticalStrip.Diagram.torusL_phaseRow_ne_zero line 509
  40. lemma OAI.CriticalStrip.Diagram.phaseRows_regular line 516