OAI/Combinatorics/LowSpaceSubsetSum/Separators/PreparedIncidenceCells.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Preparing the checker tables with a live-cell trace

The actual arrays produced by the row-at-a-time builder are placed directly in the block. The original preparation occurs only in erased proof fields. The four-block trace includes previously completed blocks while the next pair of tables is constructed.

  1. def OAI.LowSpaceSubsetSum.PreparedIncidenceCells.blockOfTables line 20
  2. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.blockOfTables_value line 51
  3. def OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepareBlock line 61
  4. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepareBlock_value line 68
  5. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepareBlock_work line 75
  6. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepareBlock_cells line 88
  7. def OAI.LowSpaceSubsetSum.PreparedIncidenceCells.payload line 95
  8. def OAI.LowSpaceSubsetSum.PreparedIncidenceCells.blockAllowance line 100

    Source documentation

    Scalar capacity; computing it does not scan either completed table.

    def blockAllowance (family : Array (Fin (2 ^ g))) : ℕ :=
…
  9. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepareBlock_payload_allowance line 103
  10. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.blockAllowance_le line 116
  11. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepareBlock_payload line 127
  12. def OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepareFour line 135
  13. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepareFour_value line 149
  14. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepareFour_work line 157
  15. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepareFour_cells line 171
  16. def OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepare line 190

    Source documentation

    The ceiling logs are computed once before the shared tables.

    def prepare (rows : Fin 4 → Vector (Fin n) g)
    (families : Fin 4 → Array (Fin (2 ^ g)))
    (hsize : ∀ i, (families i).size ≤ 11 * 2 ^ g) : (List (Block n g) × ℕ) × ℕ :=
…
  17. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepare_value line 203
  18. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepare_work line 212
  19. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepare_cells line 227
  20. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepare_work_scale line 238
  21. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepare_cells_scale line 255
  22. def OAI.LowSpaceSubsetSum.PreparedIncidenceCells.retainedInputs line 273

    Source documentation

    Four shared coordinate vectors and four sampled arrays remain resident.

    def retainedInputs (families : Fin 4 → Array (Fin (2 ^ g))) : ℕ :=
…
  23. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.retainedInputs_le line 276
  24. theorem OAI.LowSpaceSubsetSum.PreparedIncidenceCells.prepare_cells_with_inputs line 287