OAI/Combinatorics/StripMass/NodalNodes.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.cosineL line 14
  2. theorem OAI.CriticalStrip.Diagram.cosineL_map line 17
  3. theorem OAI.CriticalStrip.Diagram.twice_variableExponent_ne_neg line 25
  4. theorem OAI.CriticalStrip.Diagram.twice_variableExponent_injective line 34
  5. theorem OAI.CriticalStrip.Diagram.cosineL_two_injective line 41
  6. theorem OAI.CriticalStrip.Diagram.map_monomialL_two_variable line 55
  7. theorem OAI.CriticalStrip.Diagram.deletionBeta_laurent line 64
  8. theorem OAI.CriticalStrip.Diagram.deletionBeta_injective line 72
  9. theorem OAI.CriticalStrip.Diagram.deletionNode_sine_ne_zero line 78
  10. def OAI.CriticalStrip.Diagram.variableUnit line 102
  11. def OAI.CriticalStrip.Diagram.constantUnit line 104
  12. def OAI.CriticalStrip.Diagram.betaL line 106
  13. lemma OAI.CriticalStrip.Diagram.betaL_map line 108
  14. lemma OAI.CriticalStrip.Diagram.variableExponent_ne_neg line 111
  15. lemma OAI.CriticalStrip.Diagram.collisionRoots_injective line 116
  16. lemma OAI.CriticalStrip.Diagram.peel_betaL_self line 129
  17. lemma OAI.CriticalStrip.Diagram.insert_betaL line 146
  18. lemma OAI.CriticalStrip.Diagram.peel_betaL_other line 153
  19. lemma OAI.CriticalStrip.Diagram.variableUnit_coe line 157
  20. lemma OAI.CriticalStrip.Diagram.variableUnit_inv_coe line 159
  21. lemma OAI.CriticalStrip.Diagram.constantUnit_coe line 162
  22. lemma OAI.CriticalStrip.Diagram.constantUnit_inv_coe line 164
  23. lemma OAI.CriticalStrip.Diagram.betaL_monomial_expression line 168
  24. lemma OAI.CriticalStrip.Diagram.betaL_unit_expression line 175
  25. lemma OAI.CriticalStrip.Diagram.cosineCollisionPacket_betaL line 183
  26. lemma OAI.CriticalStrip.Diagram.betaL_difference_dvd line 205
  27. lemma OAI.CriticalStrip.Diagram.sum_upperPair line 225
  28. lemma OAI.CriticalStrip.Diagram.upperPair_incidence_sum line 235
  29. lemma OAI.CriticalStrip.Diagram.LaurentInterval.mul line 253
  30. lemma OAI.CriticalStrip.Diagram.LaurentInterval.prod_exact line 262
  31. lemma OAI.CriticalStrip.Diagram.peel_beta_coeff_self line 290
  32. lemma OAI.CriticalStrip.Diagram.peel_beta_coeff_other line 313
  33. instance OAI.CriticalStrip.Diagram.spectralFieldCharZero line 333
  34. lemma OAI.CriticalStrip.Diagram.torusCos_sum line 342
  35. lemma OAI.CriticalStrip.Diagram.torusCos_product line 348
  36. lemma OAI.CriticalStrip.Diagram.discriminant_torus_roots line 355
  37. lemma OAI.CriticalStrip.Diagram.cosineL_two_ne line 372
  38. lemma OAI.CriticalStrip.Diagram.cosineL_two_parameter line 384
  39. def OAI.CriticalStrip.Diagram.shiftedCosine line 394
  40. lemma OAI.CriticalStrip.Diagram.shiftedCosine_eq line 397
  41. lemma OAI.CriticalStrip.Diagram.shiftedCosine_ne line 401
  42. lemma OAI.CriticalStrip.Diagram.shiftedCosine_parameter line 406
  43. lemma OAI.CriticalStrip.Diagram.spectralA_shiftedCosine line 411
  44. lemma OAI.CriticalStrip.Diagram.deletionBeta_shiftedCosine line 415
  45. lemma OAI.CriticalStrip.Diagram.shiftedCosine_roots line 424
  46. lemma OAI.CriticalStrip.Diagram.shiftedCosine_discriminant_ne line 437
  47. lemma OAI.CriticalStrip.Diagram.phase_six_ne_one line 443
  48. lemma OAI.CriticalStrip.Diagram.spectralA_ne_deletionBeta line 453
  49. lemma OAI.CriticalStrip.Diagram.spectralA_roots line 465
  50. lemma OAI.CriticalStrip.Diagram.deletionBeta_roots line 472