OAI/Analysis/LaughlinGap/Certificate16.lean

GitHub source file

94 declarations, 0 contain sorry, 0 declared as axioms

Certificate16.

  1. def OAI.LaughlinGap.RealOccupation.Certificate16.keys line 17
  2. def OAI.LaughlinGap.RealOccupation.Certificate16.fibers line 18
  3. def OAI.LaughlinGap.RealOccupation.Certificate16.columns line 19
  4. def OAI.LaughlinGap.RealOccupation.Certificate16.Y line 20
  5. def OAI.LaughlinGap.RealOccupation.Certificate16.Z line 21
  6. def OAI.LaughlinGap.RealOccupation.Certificate16.W line 22
  7. def OAI.LaughlinGap.RealOccupation.Certificate16.M line 23
  8. def OAI.LaughlinGap.RealOccupation.Certificate16.L line 24
  9. def OAI.LaughlinGap.RealOccupation.Certificate16.diag line 25
  10. def OAI.LaughlinGap.RealOccupation.Certificate16.keyIndexTable line 27
  11. def OAI.LaughlinGap.RealOccupation.Certificate16.keyIndex line 28
  12. def OAI.LaughlinGap.RealOccupation.Certificate16.representatives line 30
  13. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_0 line 31
  14. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_1 line 34
  15. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_2 line 37
  16. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_3 line 40
  17. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_4 line 43
  18. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_5 line 46
  19. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_6 line 49
  20. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_7 line 52
  21. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_8 line 55
  22. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_9 line 58
  23. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_10 line 61
  24. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_11 line 64
  25. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_12 line 67
  26. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_13 line 70
  27. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_14 line 73
  28. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_15 line 76
  29. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover_16 line 79
  30. lemma OAI.LaughlinGap.RealOccupation.Certificate16.cover line 82
  31. lemma OAI.LaughlinGap.RealOccupation.Certificate16.representatives_checked line 103
  32. lemma OAI.LaughlinGap.RealOccupation.Certificate16.keys_checked line 106
  33. lemma OAI.LaughlinGap.RealOccupation.Certificate16.keys_injective line 109
  34. lemma OAI.LaughlinGap.RealOccupation.Certificate16.keys_card line 110
  35. lemma OAI.LaughlinGap.RealOccupation.Certificate16.fibers_cover line 111
  36. lemma OAI.LaughlinGap.RealOccupation.Certificate16.fibers_sound line 116
  37. lemma OAI.LaughlinGap.RealOccupation.Certificate16.fibers_checked line 120
  38. lemma OAI.LaughlinGap.RealOccupation.Certificate16.columns_checked_0 line 124
  39. lemma OAI.LaughlinGap.RealOccupation.Certificate16.columns_checked_1 line 127
  40. lemma OAI.LaughlinGap.RealOccupation.Certificate16.columns_checked_2 line 130
  41. lemma OAI.LaughlinGap.RealOccupation.Certificate16.columns_checked_3 line 133
  42. lemma OAI.LaughlinGap.RealOccupation.Certificate16.columns_checked_4 line 136
  43. lemma OAI.LaughlinGap.RealOccupation.Certificate16.columns_checked_5 line 139
  44. lemma OAI.LaughlinGap.RealOccupation.Certificate16.columns_checked_6 line 142
  45. lemma OAI.LaughlinGap.RealOccupation.Certificate16.columns_checked_7 line 145
  46. lemma OAI.LaughlinGap.RealOccupation.Certificate16.columns_checked line 148
  47. lemma OAI.LaughlinGap.RealOccupation.Certificate16.gram_checked_0 line 159
  48. lemma OAI.LaughlinGap.RealOccupation.Certificate16.gram_checked_1 line 162
  49. lemma OAI.LaughlinGap.RealOccupation.Certificate16.gram_checked_2 line 165
  50. lemma OAI.LaughlinGap.RealOccupation.Certificate16.gram_checked_3 line 168
  51. lemma OAI.LaughlinGap.RealOccupation.Certificate16.gram_checked_4 line 171
  52. lemma OAI.LaughlinGap.RealOccupation.Certificate16.gram_checked_5 line 174
  53. lemma OAI.LaughlinGap.RealOccupation.Certificate16.gram_checked_6 line 177
  54. lemma OAI.LaughlinGap.RealOccupation.Certificate16.gram_checked_7 line 180
  55. lemma OAI.LaughlinGap.RealOccupation.Certificate16.gram_checked line 183
  56. lemma OAI.LaughlinGap.RealOccupation.Certificate16.rows_table_checked_0 line 194
  57. lemma OAI.LaughlinGap.RealOccupation.Certificate16.rows_table_checked_1 line 197
  58. lemma OAI.LaughlinGap.RealOccupation.Certificate16.rows_table_checked_2 line 200
  59. lemma OAI.LaughlinGap.RealOccupation.Certificate16.rows_table_checked_3 line 203
  60. lemma OAI.LaughlinGap.RealOccupation.Certificate16.rows_table_checked_4 line 206
  61. lemma OAI.LaughlinGap.RealOccupation.Certificate16.rows_table_checked_5 line 209
  62. lemma OAI.LaughlinGap.RealOccupation.Certificate16.rows_table_checked_6 line 212
  63. lemma OAI.LaughlinGap.RealOccupation.Certificate16.rows_table_checked_7 line 215
  64. lemma OAI.LaughlinGap.RealOccupation.Certificate16.rows_table_checked line 218
  65. lemma OAI.LaughlinGap.RealOccupation.Certificate16.rows_checked line 229
  66. lemma OAI.LaughlinGap.RealOccupation.Certificate16.product_checked_0 line 232
  67. lemma OAI.LaughlinGap.RealOccupation.Certificate16.product_checked_1 line 235
  68. lemma OAI.LaughlinGap.RealOccupation.Certificate16.product_checked_2 line 238
  69. lemma OAI.LaughlinGap.RealOccupation.Certificate16.product_checked_3 line 241
  70. lemma OAI.LaughlinGap.RealOccupation.Certificate16.product_checked_4 line 244
  71. lemma OAI.LaughlinGap.RealOccupation.Certificate16.product_checked_5 line 247
  72. lemma OAI.LaughlinGap.RealOccupation.Certificate16.product_checked_6 line 250
  73. lemma OAI.LaughlinGap.RealOccupation.Certificate16.product_checked_7 line 253
  74. lemma OAI.LaughlinGap.RealOccupation.Certificate16.product_checked line 256
  75. lemma OAI.LaughlinGap.RealOccupation.Certificate16.compression_checked_0 line 267
  76. lemma OAI.LaughlinGap.RealOccupation.Certificate16.compression_checked_1 line 270
  77. lemma OAI.LaughlinGap.RealOccupation.Certificate16.compression_checked_2 line 273
  78. lemma OAI.LaughlinGap.RealOccupation.Certificate16.compression_checked_3 line 276
  79. lemma OAI.LaughlinGap.RealOccupation.Certificate16.compression_checked_4 line 279
  80. lemma OAI.LaughlinGap.RealOccupation.Certificate16.compression_checked_5 line 282
  81. lemma OAI.LaughlinGap.RealOccupation.Certificate16.compression_checked_6 line 285
  82. lemma OAI.LaughlinGap.RealOccupation.Certificate16.compression_checked_7 line 288
  83. lemma OAI.LaughlinGap.RealOccupation.Certificate16.compression_checked line 291
  84. lemma OAI.LaughlinGap.RealOccupation.Certificate16.ldl_checked_0 line 302
  85. lemma OAI.LaughlinGap.RealOccupation.Certificate16.ldl_checked_1 line 305
  86. lemma OAI.LaughlinGap.RealOccupation.Certificate16.ldl_checked_2 line 308
  87. lemma OAI.LaughlinGap.RealOccupation.Certificate16.ldl_checked_3 line 311
  88. lemma OAI.LaughlinGap.RealOccupation.Certificate16.ldl_checked_4 line 314
  89. lemma OAI.LaughlinGap.RealOccupation.Certificate16.ldl_checked_5 line 317
  90. lemma OAI.LaughlinGap.RealOccupation.Certificate16.ldl_checked_6 line 320
  91. lemma OAI.LaughlinGap.RealOccupation.Certificate16.ldl_checked_7 line 323
  92. lemma OAI.LaughlinGap.RealOccupation.Certificate16.ldl_checked line 326
  93. lemma OAI.LaughlinGap.RealOccupation.Certificate16.diag_checked line 337
  94. lemma OAI.LaughlinGap.RealOccupation.Certificate16.certificate line 338