OAI/Combinatorics/HoneycombChords/ClosedRows.lean

GitHub source file

93 declarations, 0 contain sorry, 0 declared as axioms

Four-row transfer identities and boundary contractions.

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.ClosedFourRow.middle_exchange line 18
  2. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.first_exchange line 28
  3. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.last_exchange line 38
  4. theorem OAI.CriticalHoneycomb.Transfer.ClosedFourRow.four_train line 49
  5. abbrev OAI.CriticalHoneycomb.Transfer.ClosedFourRow.Aux line 69
  6. abbrev OAI.CriticalHoneycomb.Transfer.ClosedFourRow.AuxSite line 70
  7. abbrev OAI.CriticalHoneycomb.Transfer.ClosedFourRow.Row line 71
  8. abbrev OAI.CriticalHoneycomb.Transfer.ClosedFourRow.Total line 72
  9. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.rowA line 73
  10. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.rowB line 77
  11. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.rowC line 81
  12. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.rowD line 85
  13. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exBC line 89
  14. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exBC_rowA line 93
  15. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exBC_rowD line 100
  16. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exAC line 107
  17. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exAC_rowB line 112
  18. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exAC_rowD line 119
  19. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exBD line 126
  20. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exBD_rowA line 131
  21. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exBD_rowC line 138
  22. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exAD line 145
  23. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exAD_rowB line 150
  24. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exAD_rowC line 157
  25. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.forwardPair line 164
  26. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.backwardPair line 166
  27. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairBC line 168
  28. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairBC_forward line 173
  29. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairBC_backward line 180
  30. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exBC_left line 187
  31. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exBC_right line 193
  32. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exchangeBC line 199
  33. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairAC line 206
  34. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairAC_forward line 211
  35. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairAC_backward line 218
  36. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exAC_left line 225
  37. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exAC_right line 231
  38. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exchangeAC line 237
  39. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairBD line 244
  40. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairBD_forward line 249
  41. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairBD_backward line 256
  42. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exBD_left line 263
  43. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exBD_right line 269
  44. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exchangeBD line 275
  45. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairAD line 282
  46. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairAD_forward line 287
  47. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairAD_backward line 294
  48. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exAD_left line 301
  49. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exAD_right line 307
  50. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exchangeAD line 313
  51. theorem OAI.CriticalHoneycomb.Transfer.ClosedFourRow.lifted_four_train line 321
  52. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.auxLift line 355
  53. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.leftWall line 356
  54. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.rightWall line 358
  55. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.auxLift_mul line 361
  56. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.auxLift_rightWall line 366
  57. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.leftWall_auxLift line 372
  58. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.close4 line 377
  59. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.close_train line 381
  60. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.auxBC line 401
  61. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.auxAC line 404
  62. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.auxBD line 407
  63. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.auxAD line 410
  64. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exBC_aux line 414
  65. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exAC_aux line 417
  66. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exBD_aux line 420
  67. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.exAD_aux line 423
  68. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.auxTrain line 425
  69. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.auxTrain_lift line 427
  70. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairAB line 445
  71. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairCD line 449
  72. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairAB_forward line 453
  73. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairCD_forward line 459
  74. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairAB_mul_CD line 465
  75. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairCD_mul_AB line 472
  76. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.tensorBoundary line 478
  77. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.closePair line 480
  78. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.close4_apply line 483
  79. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.sum_aux line 492
  80. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.five_sum_factor line 496
  81. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.close4_pair_product line 518
  82. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.close4_pair_reverse line 533
  83. theorem OAI.CriticalHoneycomb.Transfer.ClosedFourRow.closed_four_train line 552
  84. def OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairSwap line 588
  85. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairSwap_mulVec line 590
  86. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairSwap_sq line 594
  87. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairSwap_transpose line 599
  88. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairSwap_mul line 603
  89. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.mul_pairSwap line 607
  90. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.pairSwap_conjugate line 611
  91. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.swap_backward line 615
  92. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.closed_pair_reflection line 620
  93. lemma OAI.CriticalHoneycomb.Transfer.ClosedFourRow.closePair_dot line 638