OAI/Combinatorics/StripMass/LastRow.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

Critical honeycomb strip paths, polynomial identities and crossing mass.

  1. def OAI.CriticalStrip.Diagram.lastTile line 17
  2. theorem OAI.CriticalStrip.Diagram.Realizes.last_eq line 23
  3. def OAI.CriticalStrip.Diagram.lastCoefficient line 35
  4. theorem OAI.CriticalStrip.Diagram.lastCoefficient_map line 41
  5. theorem OAI.CriticalStrip.Diagram.rawColumn_last_factor line 51
  6. theorem OAI.CriticalStrip.Diagram.lastCoefficient_padTop line 79
  7. def OAI.CriticalStrip.Diagram.lastFactor line 88
  8. def OAI.CriticalStrip.Diagram.lastTransform line 99
  9. def OAI.CriticalStrip.Diagram.lastValue line 105
  10. theorem OAI.CriticalStrip.Diagram.rawColumn_lastValue line 113
  11. def OAI.CriticalStrip.Diagram.c line 149
  12. theorem OAI.CriticalStrip.Diagram.phase_cosine line 151
  13. theorem OAI.CriticalStrip.Diagram.phase_eight line 158
  14. theorem OAI.CriticalStrip.Diagram.constF_phase_eight line 167
  15. theorem OAI.CriticalStrip.Diagram.torusCos_inv line 170
  16. theorem OAI.CriticalStrip.Diagram.torusCos_neg line 173
  17. theorem OAI.CriticalStrip.Diagram.torusCos_phase_pow line 176
  18. theorem OAI.CriticalStrip.Diagram.torusSin_product line 181
  19. theorem OAI.CriticalStrip.Diagram.spectral_sine_pair line 194
  20. theorem OAI.CriticalStrip.Diagram.twice_rowDenominator line 207
  21. def OAI.CriticalStrip.Diagram.clearedSpectralRow line 232
  22. theorem OAI.CriticalStrip.Diagram.clearedSpectralRow_eq line 235
  23. theorem OAI.CriticalStrip.Diagram.clearedSpectralRow_vacant line 242
  24. theorem OAI.CriticalStrip.Diagram.clearedSpectralRow_cap line 246
  25. theorem OAI.CriticalStrip.Diagram.clearedSpectralRow_vertical₀ line 253
  26. theorem OAI.CriticalStrip.Diagram.clearedSpectralRow_diagonal₁ line 260
  27. def OAI.CriticalStrip.Diagram.appendZero line 275
  28. def OAI.CriticalStrip.Diagram.liftLaurentHom line 284
  29. theorem OAI.CriticalStrip.Diagram.liftLaurentHom_apply line 287
  30. theorem OAI.CriticalStrip.Diagram.appendZero_injective line 290
  31. theorem OAI.CriticalStrip.Diagram.liftLaurent_injective line 295
  32. def OAI.CriticalStrip.Diagram.liftSpectral line 300
  33. theorem OAI.CriticalStrip.Diagram.liftSpectral_evalLaurent line 306
  34. theorem OAI.CriticalStrip.Diagram.liftLaurent_monomial line 310
  35. theorem OAI.CriticalStrip.Diagram.liftLaurent_const line 314
  36. theorem OAI.CriticalStrip.Diagram.liftSpectral_const line 321
  37. theorem OAI.CriticalStrip.Diagram.appendZero_variable line 327
  38. theorem OAI.CriticalStrip.Diagram.liftSpectral_variable line 335
  39. theorem OAI.CriticalStrip.Diagram.liftSpectral_torusSin line 341
  40. theorem OAI.CriticalStrip.Diagram.liftSpectral_torusCos line 345
  41. theorem OAI.CriticalStrip.Diagram.liftSpectral_spectralA line 349
  42. theorem OAI.CriticalStrip.Diagram.evalLaurent_lastSine line 353
  43. def OAI.CriticalStrip.Diagram.Weights.map line 382
  44. lemma OAI.CriticalStrip.Diagram.Weights.map_tile line 384
  45. lemma OAI.CriticalStrip.Diagram.column_map line 388
  46. lemma OAI.CriticalStrip.Diagram.restrictedColumn_map line 397
  47. lemma OAI.CriticalStrip.Diagram.VacuumRegular.map line 403
  48. lemma OAI.CriticalStrip.Diagram.normalizedVacuum_map line 417
  49. def OAI.CriticalStrip.Diagram.permExponent line 439
  50. lemma OAI.CriticalStrip.Diagram.permExponent_injective line 444
  51. def OAI.CriticalStrip.Diagram.permLaurent line 450
  52. lemma OAI.CriticalStrip.Diagram.permLaurent_injective line 453
  53. def OAI.CriticalStrip.Diagram.permSpectral line 457
  54. lemma OAI.CriticalStrip.Diagram.permSpectral_evalLaurent line 463
  55. lemma OAI.CriticalStrip.Diagram.permLaurent_monomial line 467
  56. lemma OAI.CriticalStrip.Diagram.permSpectral_const line 471
  57. lemma OAI.CriticalStrip.Diagram.permSpectral_variable line 479
  58. lemma OAI.CriticalStrip.Diagram.permSpectral_torusSin line 490
  59. lemma OAI.CriticalStrip.Diagram.permSpectral_torusCos line 494
  60. lemma OAI.CriticalStrip.Diagram.permSpectral_torusL line 498
  61. lemma OAI.CriticalStrip.Diagram.permSpectral_torusWeights line 501
  62. lemma OAI.CriticalStrip.Diagram.permSpectral_spectralWeights line 505
  63. lemma OAI.CriticalStrip.Diagram.permSpectral_spectralA line 509
  64. lemma OAI.CriticalStrip.Diagram.permSpectral_vacuum line 512