OAI/Combinatorics/HoneycombChords/YangBaxterZero.lean

GitHub source file

252 declarations, 0 contain sorry, 0 declared as axioms

Yang–Baxter components with first spin zero.

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

  1. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101002 line 23
  2. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101020 line 32
  3. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101110 line 41
  4. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102111 line 50
  5. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110002 line 59
  6. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110011 line 68
  7. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110020 line 77
  8. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111012 line 86
  9. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111021 line 95
  10. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111102 line 104
  11. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112022 line 113
  12. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120012 line 122
  13. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120021 line 131
  14. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121022 line 140
  15. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100001 line 149
  16. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101011 line 158
  17. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101200 line 167
  18. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102012 line 176
  19. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102021 line 185
  20. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102201 line 194
  21. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102210 line 203
  22. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110101 line 212
  23. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110200 line 221
  24. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111120 line 230
  25. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111201 line 239
  26. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111210 line 248
  27. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112121 line 257
  28. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112202 line 266
  29. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112211 line 275
  30. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112220 line 284
  31. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120111 line 293
  32. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120201 line 302
  33. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120210 line 311
  34. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121112 line 320
  35. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121202 line 329
  36. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121211 line 338
  37. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121220 line 347
  38. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122221 line 356
  39. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100000 line 364
  40. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100002 line 370
  41. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100010 line 376
  42. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100011 line 382
  43. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100012 line 388
  44. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100020 line 394
  45. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100021 line 400
  46. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100022 line 406
  47. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100100 line 412
  48. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100101 line 418
  49. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100102 line 424
  50. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100110 line 430
  51. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100111 line 436
  52. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100112 line 442
  53. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100120 line 448
  54. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100121 line 454
  55. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100122 line 460
  56. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100200 line 466
  57. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100201 line 472
  58. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100202 line 478
  59. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100210 line 484
  60. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100211 line 490
  61. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100212 line 496
  62. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100220 line 502
  63. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100221 line 508
  64. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_100222 line 514
  65. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101000 line 520
  66. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101001 line 526
  67. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101010 line 532
  68. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101012 line 538
  69. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101021 line 544
  70. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101022 line 550
  71. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101100 line 556
  72. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101101 line 562
  73. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101102 line 568
  74. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101111 line 574
  75. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101112 line 580
  76. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101120 line 586
  77. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101121 line 592
  78. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101122 line 598
  79. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101201 line 604
  80. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101202 line 610
  81. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101210 line 616
  82. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101211 line 622
  83. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101212 line 628
  84. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101220 line 634
  85. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101221 line 640
  86. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_101222 line 646
  87. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102000 line 652
  88. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102001 line 658
  89. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102002 line 664
  90. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102010 line 670
  91. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102011 line 676
  92. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102020 line 682
  93. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102022 line 688
  94. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102100 line 694
  95. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102101 line 700
  96. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102102 line 706
  97. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102110 line 712
  98. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102112 line 718
  99. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102120 line 724
  100. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102121 line 730
  101. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102122 line 736
  102. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102200 line 742
  103. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102202 line 748
  104. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102211 line 754
  105. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102212 line 760
  106. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102220 line 766
  107. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102221 line 772
  108. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_102222 line 778
  109. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110000 line 784
  110. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110001 line 790
  111. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110010 line 796
  112. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110012 line 802
  113. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110021 line 808
  114. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110022 line 814
  115. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110100 line 820
  116. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110102 line 826
  117. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110110 line 832
  118. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110111 line 838
  119. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110112 line 844
  120. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110120 line 850
  121. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110121 line 856
  122. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110122 line 862
  123. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110201 line 868
  124. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110202 line 874
  125. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110210 line 880
  126. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110211 line 886
  127. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110212 line 892
  128. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110220 line 898
  129. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110221 line 904
  130. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_110222 line 910
  131. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111000 line 916
  132. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111001 line 922
  133. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111002 line 928
  134. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111010 line 934
  135. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111011 line 940
  136. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111020 line 946
  137. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111022 line 952
  138. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111100 line 958
  139. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111101 line 964
  140. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111110 line 970
  141. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111111 line 976
  142. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111112 line 982
  143. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111121 line 988
  144. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111122 line 994
  145. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111200 line 1000
  146. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111202 line 1006
  147. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111211 line 1012
  148. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111212 line 1018
  149. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111220 line 1024
  150. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111221 line 1030
  151. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_111222 line 1036
  152. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112000 line 1042
  153. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112001 line 1048
  154. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112002 line 1054
  155. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112010 line 1060
  156. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112011 line 1066
  157. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112012 line 1072
  158. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112020 line 1078
  159. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112021 line 1084
  160. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112100 line 1090
  161. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112101 line 1096
  162. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112102 line 1102
  163. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112110 line 1108
  164. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112111 line 1114
  165. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112112 line 1120
  166. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112120 line 1126
  167. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112122 line 1132
  168. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112200 line 1138
  169. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112201 line 1144
  170. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112210 line 1150
  171. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112212 line 1156
  172. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112221 line 1162
  173. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_112222 line 1168
  174. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120000 line 1174
  175. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120001 line 1180
  176. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120002 line 1186
  177. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120010 line 1192
  178. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120011 line 1198
  179. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120020 line 1204
  180. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120022 line 1210
  181. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120100 line 1216
  182. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120101 line 1222
  183. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120102 line 1228
  184. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120110 line 1234
  185. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120112 line 1240
  186. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120120 line 1246
  187. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120121 line 1252
  188. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120122 line 1258
  189. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120200 line 1264
  190. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120202 line 1270
  191. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120211 line 1276
  192. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120212 line 1282
  193. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120220 line 1288
  194. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120221 line 1294
  195. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_120222 line 1300
  196. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121000 line 1306
  197. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121001 line 1312
  198. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121002 line 1318
  199. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121010 line 1324
  200. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121011 line 1330
  201. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121012 line 1336
  202. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121020 line 1342
  203. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121021 line 1348
  204. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121100 line 1354
  205. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121101 line 1360
  206. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121102 line 1366
  207. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121110 line 1372
  208. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121111 line 1378
  209. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121120 line 1384
  210. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121121 line 1390
  211. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121122 line 1396
  212. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121200 line 1402
  213. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121201 line 1408
  214. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121210 line 1414
  215. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121212 line 1420
  216. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121221 line 1426
  217. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_121222 line 1432
  218. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122000 line 1438
  219. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122001 line 1444
  220. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122002 line 1450
  221. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122010 line 1456
  222. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122011 line 1462
  223. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122012 line 1468
  224. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122020 line 1474
  225. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122021 line 1480
  226. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122022 line 1486
  227. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122100 line 1492
  228. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122101 line 1498
  229. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122102 line 1504
  230. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122110 line 1510
  231. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122111 line 1516
  232. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122112 line 1522
  233. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122120 line 1528
  234. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122121 line 1534
  235. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122122 line 1540
  236. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122200 line 1546
  237. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122201 line 1552
  238. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122202 line 1558
  239. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122210 line 1564
  240. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122211 line 1570
  241. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122212 line 1576
  242. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122220 line 1582
  243. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.component_122222 line 1588
  244. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_100 line 1595
  245. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_101 line 1628
  246. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_102 line 1661
  247. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_110 line 1694
  248. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_111 line 1727
  249. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_112 line 1760
  250. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_120 line 1793
  251. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_121 line 1826
  252. lemma OAI.CriticalHoneycomb.Transfer.YangBaxter.block_122 line 1859