OAI/Combinatorics/HoneycombChords/YangBaxterPolynomialsNegative.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

Yang–Baxter polynomial reductions with first spin negative.

This development follows the finite strip transfer calculation for critical honeycomb walks in the companion paper on uniform marked polygon estimates.

  1. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200002_0 line 19
  2. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200002_1 line 22
  3. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200002_2 line 25
  4. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_200002_3 line 29
  5. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200002_3 line 36
  6. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200002_4 line 39
  7. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_200002_4 line 43
  8. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200002_5 line 50
  9. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200002_6 line 53
  10. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_200002_5 line 57
  11. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200002_7 line 64
  12. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200002_8 line 67
  13. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_200002_0 line 71
  14. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200002_9 line 78
  15. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200002_10 line 81
  16. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_200002_1 line 85
  17. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200002_11 line 92
  18. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_200002_2 line 96
  19. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_200002 line 104
  20. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200011_0 line 113
  21. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200011_1 line 116
  22. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200011_2 line 119
  23. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_200011_3 line 123
  24. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200011_3 line 130
  25. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200011_4 line 133
  26. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_200011_4 line 137
  27. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200011_5 line 144
  28. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200011_6 line 147
  29. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_200011_5 line 151
  30. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200011_7 line 158
  31. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200011_8 line 161
  32. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_200011_0 line 165
  33. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200011_9 line 172
  34. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200011_10 line 175
  35. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_200011_1 line 179
  36. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_200011_11 line 186
  37. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_200011_2 line 190
  38. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_200011 line 198
  39. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_201012_0 line 207
  40. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_201012_1 line 210
  41. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_201012_2 line 213
  42. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_201012_3 line 217
  43. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_201012_3 line 224
  44. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_201012_4 line 227
  45. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_201012_4 line 231
  46. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_201012_5 line 238
  47. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_201012_6 line 241
  48. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_201012_5 line 245
  49. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_201012_7 line 252
  50. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_201012_8 line 255
  51. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_201012_0 line 259
  52. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_201012_9 line 266
  53. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_201012_10 line 269
  54. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_201012_1 line 273
  55. def OAI.CriticalHoneycomb.Transfer.YangBaxter.poly_201012_11 line 280
  56. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.reduce_201012_2 line 284
  57. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.polynomial_201012 line 292