OAI/Analysis/LaughlinGap/Certificate22.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

Certificate22.

  1. def OAI.LaughlinGap.RealOccupation.Certificate22.keys line 17
  2. def OAI.LaughlinGap.RealOccupation.Certificate22.fibers line 18
  3. def OAI.LaughlinGap.RealOccupation.Certificate22.columns line 19
  4. def OAI.LaughlinGap.RealOccupation.Certificate22.Y line 20
  5. def OAI.LaughlinGap.RealOccupation.Certificate22.Z line 21
  6. def OAI.LaughlinGap.RealOccupation.Certificate22.W line 22
  7. def OAI.LaughlinGap.RealOccupation.Certificate22.M line 23
  8. def OAI.LaughlinGap.RealOccupation.Certificate22.L line 24
  9. def OAI.LaughlinGap.RealOccupation.Certificate22.diag line 25
  10. def OAI.LaughlinGap.RealOccupation.Certificate22.keyIndexTable line 27
  11. def OAI.LaughlinGap.RealOccupation.Certificate22.keyIndex line 28
  12. def OAI.LaughlinGap.RealOccupation.Certificate22.representatives line 30
  13. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_0 line 31
  14. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_1 line 34
  15. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_2 line 37
  16. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_3 line 40
  17. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_4 line 43
  18. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_5 line 46
  19. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_6 line 49
  20. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_7 line 52
  21. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_8 line 55
  22. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_9 line 58
  23. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_10 line 61
  24. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_11 line 64
  25. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_12 line 67
  26. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_13 line 70
  27. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_14 line 73
  28. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_15 line 76
  29. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_16 line 79
  30. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_17 line 82
  31. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_18 line 85
  32. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_19 line 88
  33. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_20 line 91
  34. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_21 line 94
  35. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover_22 line 97
  36. lemma OAI.LaughlinGap.RealOccupation.Certificate22.cover line 100
  37. lemma OAI.LaughlinGap.RealOccupation.Certificate22.representatives_checked line 127
  38. lemma OAI.LaughlinGap.RealOccupation.Certificate22.keys_checked line 130
  39. lemma OAI.LaughlinGap.RealOccupation.Certificate22.keys_injective line 133
  40. lemma OAI.LaughlinGap.RealOccupation.Certificate22.keys_card line 134
  41. lemma OAI.LaughlinGap.RealOccupation.Certificate22.fibers_cover line 135
  42. lemma OAI.LaughlinGap.RealOccupation.Certificate22.fibers_sound line 140
  43. lemma OAI.LaughlinGap.RealOccupation.Certificate22.fibers_checked line 144
  44. lemma OAI.LaughlinGap.RealOccupation.Certificate22.columns_checked_0 line 148
  45. lemma OAI.LaughlinGap.RealOccupation.Certificate22.columns_checked_1 line 151
  46. lemma OAI.LaughlinGap.RealOccupation.Certificate22.columns_checked_2 line 154
  47. lemma OAI.LaughlinGap.RealOccupation.Certificate22.columns_checked_3 line 157
  48. lemma OAI.LaughlinGap.RealOccupation.Certificate22.columns_checked_4 line 160
  49. lemma OAI.LaughlinGap.RealOccupation.Certificate22.columns_checked_5 line 163
  50. lemma OAI.LaughlinGap.RealOccupation.Certificate22.columns_checked_6 line 166
  51. lemma OAI.LaughlinGap.RealOccupation.Certificate22.columns_checked_7 line 169
  52. lemma OAI.LaughlinGap.RealOccupation.Certificate22.columns_checked_8 line 172
  53. lemma OAI.LaughlinGap.RealOccupation.Certificate22.columns_checked_9 line 175
  54. lemma OAI.LaughlinGap.RealOccupation.Certificate22.columns_checked_10 line 178
  55. lemma OAI.LaughlinGap.RealOccupation.Certificate22.columns_checked line 181
  56. lemma OAI.LaughlinGap.RealOccupation.Certificate22.gram_checked_0 line 195
  57. lemma OAI.LaughlinGap.RealOccupation.Certificate22.gram_checked_1 line 198
  58. lemma OAI.LaughlinGap.RealOccupation.Certificate22.gram_checked_2 line 201
  59. lemma OAI.LaughlinGap.RealOccupation.Certificate22.gram_checked_3 line 204
  60. lemma OAI.LaughlinGap.RealOccupation.Certificate22.gram_checked_4 line 207
  61. lemma OAI.LaughlinGap.RealOccupation.Certificate22.gram_checked_5 line 210
  62. lemma OAI.LaughlinGap.RealOccupation.Certificate22.gram_checked_6 line 213
  63. lemma OAI.LaughlinGap.RealOccupation.Certificate22.gram_checked_7 line 216
  64. lemma OAI.LaughlinGap.RealOccupation.Certificate22.gram_checked_8 line 219
  65. lemma OAI.LaughlinGap.RealOccupation.Certificate22.gram_checked_9 line 222
  66. lemma OAI.LaughlinGap.RealOccupation.Certificate22.gram_checked_10 line 225
  67. lemma OAI.LaughlinGap.RealOccupation.Certificate22.gram_checked line 228
  68. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_table_checked_0 line 242
  69. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_table_checked_1 line 245
  70. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_table_checked_2 line 248
  71. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_table_checked_3 line 251
  72. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_table_checked_4 line 254
  73. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_table_checked_5 line 257
  74. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_table_checked_6 line 260
  75. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_table_checked_7 line 263
  76. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_table_checked_8 line 266
  77. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_table_checked_9 line 269
  78. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_table_checked_10 line 272
  79. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_table_checked line 275
  80. lemma OAI.LaughlinGap.RealOccupation.Certificate22.rows_checked line 289
  81. lemma OAI.LaughlinGap.RealOccupation.Certificate22.product_checked_0 line 292
  82. lemma OAI.LaughlinGap.RealOccupation.Certificate22.product_checked_1 line 295
  83. lemma OAI.LaughlinGap.RealOccupation.Certificate22.product_checked_2 line 298
  84. lemma OAI.LaughlinGap.RealOccupation.Certificate22.product_checked_3 line 301
  85. lemma OAI.LaughlinGap.RealOccupation.Certificate22.product_checked_4 line 304
  86. lemma OAI.LaughlinGap.RealOccupation.Certificate22.product_checked_5 line 307
  87. lemma OAI.LaughlinGap.RealOccupation.Certificate22.product_checked_6 line 310
  88. lemma OAI.LaughlinGap.RealOccupation.Certificate22.product_checked_7 line 313
  89. lemma OAI.LaughlinGap.RealOccupation.Certificate22.product_checked_8 line 316
  90. lemma OAI.LaughlinGap.RealOccupation.Certificate22.product_checked_9 line 319
  91. lemma OAI.LaughlinGap.RealOccupation.Certificate22.product_checked_10 line 322
  92. lemma OAI.LaughlinGap.RealOccupation.Certificate22.product_checked line 325
  93. lemma OAI.LaughlinGap.RealOccupation.Certificate22.compression_checked_0 line 339
  94. lemma OAI.LaughlinGap.RealOccupation.Certificate22.compression_checked_1 line 342
  95. lemma OAI.LaughlinGap.RealOccupation.Certificate22.compression_checked_2 line 345
  96. lemma OAI.LaughlinGap.RealOccupation.Certificate22.compression_checked_3 line 348
  97. lemma OAI.LaughlinGap.RealOccupation.Certificate22.compression_checked_4 line 351
  98. lemma OAI.LaughlinGap.RealOccupation.Certificate22.compression_checked_5 line 354
  99. lemma OAI.LaughlinGap.RealOccupation.Certificate22.compression_checked_6 line 357
  100. lemma OAI.LaughlinGap.RealOccupation.Certificate22.compression_checked_7 line 360
  101. lemma OAI.LaughlinGap.RealOccupation.Certificate22.compression_checked_8 line 363
  102. lemma OAI.LaughlinGap.RealOccupation.Certificate22.compression_checked_9 line 366
  103. lemma OAI.LaughlinGap.RealOccupation.Certificate22.compression_checked_10 line 369
  104. lemma OAI.LaughlinGap.RealOccupation.Certificate22.compression_checked line 372
  105. lemma OAI.LaughlinGap.RealOccupation.Certificate22.ldl_checked_0 line 386
  106. lemma OAI.LaughlinGap.RealOccupation.Certificate22.ldl_checked_1 line 389
  107. lemma OAI.LaughlinGap.RealOccupation.Certificate22.ldl_checked_2 line 392
  108. lemma OAI.LaughlinGap.RealOccupation.Certificate22.ldl_checked_3 line 395
  109. lemma OAI.LaughlinGap.RealOccupation.Certificate22.ldl_checked_4 line 398
  110. lemma OAI.LaughlinGap.RealOccupation.Certificate22.ldl_checked_5 line 401
  111. lemma OAI.LaughlinGap.RealOccupation.Certificate22.ldl_checked_6 line 404
  112. lemma OAI.LaughlinGap.RealOccupation.Certificate22.ldl_checked_7 line 407
  113. lemma OAI.LaughlinGap.RealOccupation.Certificate22.ldl_checked_8 line 410
  114. lemma OAI.LaughlinGap.RealOccupation.Certificate22.ldl_checked_9 line 413
  115. lemma OAI.LaughlinGap.RealOccupation.Certificate22.ldl_checked_10 line 416
  116. lemma OAI.LaughlinGap.RealOccupation.Certificate22.ldl_checked line 419
  117. lemma OAI.LaughlinGap.RealOccupation.Certificate22.diag_checked line 433
  118. lemma OAI.LaughlinGap.RealOccupation.Certificate22.certificate line 434