OAI/Combinatorics/LowSpaceSubsetSum/Separators/StoredIncidenceBuild.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Executed construction of the separator's stored incidence lists

Sampled local masks are stored as bounded integer bit codes. Containment and avoidance use bitwise intersection. Every table row scans the sampled family in order and retains its occurrence indices, including duplicates.

  1. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.mem_decode line 17
  2. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.outside line 24
  3. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.subset_iff line 28
  4. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.disjoint_iff line 48
  5. def OAI.LowSpaceSubsetSum.StoredIncidenceBuild.contains line 73
  6. def OAI.LowSpaceSubsetSum.StoredIncidenceBuild.avoids line 75
  7. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.contains_value line 77
  8. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.avoids_value line 81
  9. def OAI.LowSpaceSubsetSum.StoredIncidenceBuild.row line 85
  10. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.row_value line 91
  11. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.row_work line 98
  12. def OAI.LowSpaceSubsetSum.StoredIncidenceBuild.mapAcc line 110
  13. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.mapAcc_value line 116
  14. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.mapAcc_work line 123
  15. def OAI.LowSpaceSubsetSum.StoredIncidenceBuild.preprocess line 134
  16. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.preprocess_value line 139
  17. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.preprocess_size line 148
  18. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.preprocess_get line 153
  19. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.preprocess_work line 159
  20. def OAI.LowSpaceSubsetSum.StoredIncidenceBuild.tables line 168
  21. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.tables_work line 173
  22. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.table_map line 180
  23. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.containsStore_value line 197
  24. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.avoidsStore_value line 207
  25. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.tables_value line 217
  26. theorem OAI.LowSpaceSubsetSum.StoredIncidenceBuild.tables_work_of_size line 224

    Source documentation

    The full preprocessing is below a constant times the stored table capacity.

    theorem tables_work_of_size (family : Array (Fin (2 ^ g)))
    (hsize : family.size ≤ 11 * 2 ^ g) :
    (tables family).2 ≤ 220 * 2 ^ (2 * g) := by
…

    Mentions: OAI.LowSpaceSubsetSum.StoredIncidenceBuild.tables