OAI/Combinatorics/LowSpaceSubsetSum/Separators/IncidenceBuildCells.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

Live cells while building the shared incidence tables

Rows are constructed one at a time. The tail-recursive table builder retains completed row arrays, a pointer accumulator, and one active row. The payload counter is cached; no traversal of completed rows is needed.

  1. def OAI.LowSpaceSubsetSum.IncidenceBuildCells.row line 17
  2. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.row_value line 24
  3. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.row_cells line 29
  4. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.row_size line 40
  5. def OAI.LowSpaceSubsetSum.IncidenceBuildCells.mapAcc line 46
  6. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.mapAcc_value line 56
  7. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.mapAcc_work line 63
  8. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.mapAcc_cells line 78
  9. def OAI.LowSpaceSubsetSum.IncidenceBuildCells.preprocess line 98

    Source documentation

    Same completed table as the source builder, with an additional cell trace; the cached payload count changes only when a row is stored.

    def preprocess (test : Fin (2 ^ g) → Fin (2 ^ g) → (Bool × ℕ) × ℕ)
    (family : Array (Fin (2 ^ g))) : (Array (Array ℕ) × ℕ) × ℕ :=
…
  10. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.preprocess_value line 103
  11. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.preprocess_work line 113
  12. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.preprocess_cells line 124
  13. def OAI.LowSpaceSubsetSum.IncidenceBuildCells.arrayCells line 142
  14. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.preprocess_payload line 144
  15. def OAI.LowSpaceSubsetSum.IncidenceBuildCells.contains line 156
  16. def OAI.LowSpaceSubsetSum.IncidenceBuildCells.avoids line 157
  17. def OAI.LowSpaceSubsetSum.IncidenceBuildCells.tables line 159
  18. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.tables_value line 166
  19. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.tables_work line 170
  20. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.one_table_cells line 177
  21. theorem OAI.LowSpaceSubsetSum.IncidenceBuildCells.tables_cells line 189