OAI/Combinatorics/StripMass/PhaseAlgebra.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.phase_four line 15
  2. theorem OAI.CriticalStrip.Diagram.constF_phase_four line 25
  3. theorem OAI.CriticalStrip.Diagram.constF_d_eq line 29
  4. def OAI.CriticalStrip.Diagram.torusCommon line 44
  5. theorem OAI.CriticalStrip.Diagram.torusCommon_eq line 47
  6. theorem OAI.CriticalStrip.Diagram.torusCommon_ne_zero line 56
  7. theorem OAI.CriticalStrip.Diagram.ThreeBox.torusWeights_cleared line 77
  8. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_scale line 101
  9. theorem OAI.CriticalStrip.Diagram.ThreeBox.braid_coefficient line 113
  10. theorem OAI.CriticalStrip.Diagram.ThreeBox.coefficient_eq_sumif line 145
  11. theorem OAI.CriticalStrip.Diagram.ThreeBox.profile_partition line 156
  12. theorem OAI.CriticalStrip.Diagram.ThreeBox.patch_partition line 184
  13. theorem OAI.CriticalStrip.Diagram.ThreeBox.braid_partition line 196
  14. theorem OAI.CriticalStrip.Diagram.ThreeBox.split3_numerator line 225
  15. theorem OAI.CriticalStrip.Diagram.ThreeBox.split2_numerator line 282
  16. def OAI.CriticalStrip.Diagram.swapWeights line 350
  17. def OAI.CriticalStrip.Diagram.mergeWeights line 353
  18. lemma OAI.CriticalStrip.Diagram.swapWeights_tile line 356
  19. lemma OAI.CriticalStrip.Diagram.deletionWeights_tile line 358
  20. lemma OAI.CriticalStrip.Diagram.eighthRoot_two_add_one_ne_zero line 361
  21. lemma OAI.CriticalStrip.Diagram.mergeWeights_cleared line 371
  22. lemma OAI.CriticalStrip.Diagram.ThreeBox.coefficient_scale₂₃ line 377
  23. lemma OAI.CriticalStrip.Diagram.ThreeBox.coefficient_scale₁₃ line 383
  24. lemma OAI.CriticalStrip.Diagram.ThreeBox.coefficient_deletion line 389
  25. lemma OAI.CriticalStrip.Diagram.ThreeBox.coefficient_merge line 410
  26. lemma OAI.CriticalStrip.Diagram.rho_eq_inv_two_C line 450
  27. lemma OAI.CriticalStrip.Diagram.phase_div_two_add_one line 455
  28. lemma OAI.CriticalStrip.Diagram.mergeWeights_source_constant line 472
  29. lemma OAI.CriticalStrip.Diagram.torusSin_inv line 487
  30. lemma OAI.CriticalStrip.Diagram.torusSin_neg line 491
  31. lemma OAI.CriticalStrip.Diagram.shifted_gamma_difference line 495
  32. lemma OAI.CriticalStrip.Diagram.shifted_sigma_difference line 524
  33. theorem OAI.CriticalStrip.Diagram.movingBox_scalar_cancellation line 552