OAI/Combinatorics/HoneycombChords/BoundaryFusionEquation.lean

GitHub source file

84 declarations, 0 contain sorry, 0 declared as axioms

Polynomial boundary fusion identities for the honeycomb strip transfer. The fusion maps preserve the exact boundary normalization.

  1. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.wNum line 11
  2. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.wBarNum line 21
  3. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.bNum line 31
  4. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.aNum line 32
  5. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.fusionL0 line 33
  6. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.fusionL1 line 36
  7. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.fusionR0 line 41
  8. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.fusionR1 line 43
  9. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.slot2_constant_rect line 45
  10. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.slot2_linear_rect line 49
  11. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.core0_rect line 56
  12. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.core1_rect line 61
  13. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionAdd line 68
  14. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionMul line 69
  15. abbrev OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionPow line 70
  16. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0000 line 74
  17. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0001 line 78
  18. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0002 line 82
  19. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate0010 line 86
  20. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0010 line 89
  21. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0011 line 96
  22. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0012 line 100
  23. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0020 line 104
  24. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate0021 line 108
  25. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0021 line 111
  26. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0022 line 118
  27. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate0100 line 122
  28. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0100 line 125
  29. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0101 line 132
  30. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0102 line 136
  31. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0110 line 140
  32. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate0111 line 144
  33. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0111 line 147
  34. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0112 line 154
  35. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0120 line 158
  36. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0121 line 162
  37. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate0122 line 166
  38. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0122 line 169
  39. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0200 line 176
  40. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate0201 line 180
  41. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0201 line 183
  42. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0202 line 190
  43. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0210 line 194
  44. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0211 line 198
  45. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate0212 line 202
  46. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0212 line 205
  47. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0220 line 212
  48. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0221 line 216
  49. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent0222 line 220
  50. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate1000 line 224
  51. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1000 line 227
  52. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1001 line 234
  53. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1002 line 238
  54. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1010 line 242
  55. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate1011 line 246
  56. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1011 line 249
  57. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1012 line 256
  58. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1020 line 260
  59. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1021 line 264
  60. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate1022 line 268
  61. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1022 line 271
  62. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1100 line 278
  63. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate1101 line 282
  64. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1101 line 285
  65. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1102 line 292
  66. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1110 line 296
  67. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1111 line 300
  68. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate1112 line 304
  69. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1112 line 307
  70. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1120 line 314
  71. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1121 line 318
  72. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1122 line 322
  73. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1200 line 326
  74. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1201 line 330
  75. def OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionCertificate1202 line 334
  76. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1202 line 337
  77. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1210 line 344
  78. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1211 line 348
  79. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1212 line 352
  80. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1220 line 356
  81. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1221 line 360
  82. lemma OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.boundaryFusionComponent1222 line 364
  83. theorem OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.source_numerator0 line 369
  84. theorem OAI.CriticalHoneycomb.Transfer.Reflection.Fusion.source_numerator1 line 401