OAI/Combinatorics/StripMass/RootOfUnityPowers.lean

GitHub source file

74 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. theorem OAI.CriticalStrip.Diagram.eighthRoot_power line 12
  2. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_8 line 19
  3. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_9 line 25
  4. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_10 line 31
  5. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_11 line 37
  6. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_12 line 43
  7. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_13 line 49
  8. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_14 line 55
  9. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_15 line 61
  10. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_16 line 67
  11. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_17 line 73
  12. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_18 line 79
  13. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_19 line 85
  14. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_20 line 91
  15. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_21 line 97
  16. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_22 line 103
  17. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_23 line 109
  18. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_24 line 115
  19. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_25 line 121
  20. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_26 line 127
  21. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_27 line 133
  22. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_28 line 139
  23. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_29 line 145
  24. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_30 line 151
  25. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_31 line 157
  26. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_32 line 163
  27. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_33 line 169
  28. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_34 line 175
  29. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_35 line 181
  30. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_36 line 187
  31. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_37 line 193
  32. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_38 line 199
  33. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_39 line 205
  34. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_40 line 211
  35. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_41 line 217
  36. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_42 line 223
  37. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_43 line 229
  38. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_44 line 235
  39. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_45 line 241
  40. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_46 line 247
  41. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_47 line 253
  42. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_48 line 259
  43. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_49 line 271
  44. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_50 line 277
  45. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_51 line 283
  46. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_52 line 289
  47. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_53 line 295
  48. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_54 line 301
  49. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_55 line 307
  50. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_56 line 313
  51. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_57 line 319
  52. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_58 line 325
  53. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_59 line 331
  54. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_60 line 337
  55. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_61 line 343
  56. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_62 line 349
  57. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_63 line 355
  58. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_64 line 361
  59. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_65 line 367
  60. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_66 line 373
  61. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_67 line 379
  62. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_68 line 385
  63. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_69 line 391
  64. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_70 line 397
  65. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_71 line 403
  66. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_72 line 409
  67. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_73 line 415
  68. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_74 line 421
  69. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_75 line 427
  70. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_76 line 433
  71. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_77 line 439
  72. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_78 line 445
  73. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_79 line 451
  74. theorem OAI.CriticalStrip.Diagram.eighthRoot_power_80 line 457