OAI/Analysis/LaughlinGap/Certificate23.lean

GitHub source file

125 declarations, 0 contain sorry, 0 declared as axioms

Certificate23.

  1. def OAI.LaughlinGap.RealOccupation.Certificate23.keys line 19
  2. def OAI.LaughlinGap.RealOccupation.Certificate23.fibers line 20
  3. def OAI.LaughlinGap.RealOccupation.Certificate23.columns line 21
  4. def OAI.LaughlinGap.RealOccupation.Certificate23.Y line 22
  5. def OAI.LaughlinGap.RealOccupation.Certificate23.Z line 23
  6. def OAI.LaughlinGap.RealOccupation.Certificate23.W line 24
  7. def OAI.LaughlinGap.RealOccupation.Certificate23.M line 25
  8. def OAI.LaughlinGap.RealOccupation.Certificate23.L line 26
  9. def OAI.LaughlinGap.RealOccupation.Certificate23.diag line 27
  10. def OAI.LaughlinGap.RealOccupation.Certificate23.keyIndexTable line 29
  11. def OAI.LaughlinGap.RealOccupation.Certificate23.keyIndex line 30
  12. def OAI.LaughlinGap.RealOccupation.Certificate23.representatives line 32
  13. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_0 line 33
  14. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_1 line 36
  15. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_2 line 39
  16. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_3 line 42
  17. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_4 line 45
  18. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_5 line 48
  19. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_6 line 51
  20. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_7 line 54
  21. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_8 line 57
  22. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_9 line 60
  23. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_10 line 63
  24. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_11 line 66
  25. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_12 line 69
  26. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_13 line 72
  27. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_14 line 75
  28. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_15 line 78
  29. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_16 line 81
  30. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_17 line 84
  31. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_18 line 87
  32. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_19 line 90
  33. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_20 line 93
  34. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_21 line 96
  35. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_22 line 99
  36. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover_23 line 102
  37. lemma OAI.LaughlinGap.RealOccupation.Certificate23.cover line 105
  38. lemma OAI.LaughlinGap.RealOccupation.Certificate23.representatives_checked line 133
  39. lemma OAI.LaughlinGap.RealOccupation.Certificate23.keys_checked line 136
  40. lemma OAI.LaughlinGap.RealOccupation.Certificate23.keys_injective line 139
  41. lemma OAI.LaughlinGap.RealOccupation.Certificate23.keys_card line 140
  42. lemma OAI.LaughlinGap.RealOccupation.Certificate23.fibers_cover line 141
  43. lemma OAI.LaughlinGap.RealOccupation.Certificate23.fibers_sound line 146
  44. lemma OAI.LaughlinGap.RealOccupation.Certificate23.fibers_checked line 150
  45. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked_0 line 154
  46. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked_1 line 157
  47. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked_2 line 160
  48. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked_3 line 163
  49. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked_4 line 166
  50. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked_5 line 169
  51. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked_6 line 172
  52. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked_7 line 175
  53. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked_8 line 178
  54. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked_9 line 181
  55. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked_10 line 184
  56. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked_11 line 187
  57. lemma OAI.LaughlinGap.RealOccupation.Certificate23.columns_checked line 190
  58. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked_0 line 205
  59. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked_1 line 208
  60. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked_2 line 211
  61. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked_3 line 214
  62. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked_4 line 217
  63. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked_5 line 220
  64. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked_6 line 223
  65. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked_7 line 226
  66. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked_8 line 229
  67. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked_9 line 232
  68. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked_10 line 235
  69. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked_11 line 238
  70. lemma OAI.LaughlinGap.RealOccupation.Certificate23.gram_checked line 241
  71. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked_0 line 256
  72. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked_1 line 259
  73. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked_2 line 262
  74. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked_3 line 265
  75. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked_4 line 268
  76. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked_5 line 271
  77. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked_6 line 274
  78. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked_7 line 277
  79. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked_8 line 280
  80. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked_9 line 283
  81. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked_10 line 286
  82. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked_11 line 289
  83. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_table_checked line 292
  84. lemma OAI.LaughlinGap.RealOccupation.Certificate23.rows_checked line 307
  85. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked_0 line 310
  86. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked_1 line 313
  87. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked_2 line 316
  88. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked_3 line 319
  89. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked_4 line 322
  90. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked_5 line 325
  91. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked_6 line 328
  92. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked_7 line 331
  93. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked_8 line 334
  94. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked_9 line 337
  95. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked_10 line 340
  96. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked_11 line 343
  97. lemma OAI.LaughlinGap.RealOccupation.Certificate23.product_checked line 346
  98. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked_0 line 361
  99. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked_1 line 364
  100. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked_2 line 367
  101. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked_3 line 370
  102. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked_4 line 373
  103. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked_5 line 376
  104. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked_6 line 379
  105. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked_7 line 382
  106. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked_8 line 385
  107. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked_9 line 388
  108. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked_10 line 391
  109. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked_11 line 394
  110. lemma OAI.LaughlinGap.RealOccupation.Certificate23.compression_checked line 397
  111. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked_0 line 412
  112. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked_1 line 415
  113. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked_2 line 418
  114. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked_3 line 421
  115. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked_4 line 424
  116. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked_5 line 427
  117. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked_6 line 430
  118. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked_7 line 433
  119. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked_8 line 436
  120. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked_9 line 439
  121. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked_10 line 442
  122. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked_11 line 445
  123. lemma OAI.LaughlinGap.RealOccupation.Certificate23.ldl_checked line 448
  124. lemma OAI.LaughlinGap.RealOccupation.Certificate23.diag_checked line 463
  125. lemma OAI.LaughlinGap.RealOccupation.Certificate23.certificate line 464