OAI/Combinatorics/LowSpaceSubsetSum/Separators/StoredSeparatorCheck.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

A measured separator checker on stored dictionaries

Each block retains its coordinate vector and both incidence tables. The recursive checker passes those fixed tables to the measured DFS; only record-pointer lists are filtered or sorted during individual checks.

  1. structure OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block line 20
  2. def OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.left line 39
  3. def OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.right line 42
  4. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.left_sorted line 45
  5. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.right_sorted line 50
  6. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.left_bound line 55
  7. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.right_bound line 60
  8. def OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.source line 65
  9. def OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.leftQuery line 72
  10. def OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.rightQuery line 77
  11. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.leftQuery_value line 82
  12. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.rightQuery_value line 86
  13. def OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.queryBound line 90
  14. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.leftQuery_work line 92
  15. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.rightQuery_work line 101
  16. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.preprocess_sorted line 112
  17. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.preprocess_bound line 124
  18. def OAI.LowSpaceSubsetSum.StoredSeparatorCheck.prepareBlock line 135

    Source documentation

    The table construction runs once for this block.

    def prepareBlock (row : Vector (Fin n) g) (family : Array (Fin (2 ^ g)))
    (depth steps : ℕ) (hd : depth = Nat.clog 2 family.size)
    (hs : family.size < 2 ^ steps) : Block n g × ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block

  19. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.prepareBlock_work line 149
  20. def OAI.LowSpaceSubsetSum.StoredSeparatorCheck.prepareFour line 156

    Source documentation

    Four preparations are shared by every dictionary check in this trial.

    def prepareFour (rows : Fin 4 → Vector (Fin n) g)
    (families : Fin 4 → Array (Fin (2 ^ g))) (depths steps : Fin 4 → ℕ)
    (hd : ∀ i, depths i = Nat.clog 2 (families i).size)
    (hs : ∀ i, (families i).size < 2 ^ steps i) : List (Block n g) × ℕ :=
…

    Mentions: OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block

  21. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.prepareFour_value line 166
  22. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.prepareFour_length line 173
  23. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.prepareFour_work line 179
  24. def OAI.LowSpaceSubsetSum.StoredSeparatorCheck.run line 193

    Source documentation

    The capacity is supplied once; guards charge their two list-length scans.

    def run (capacity : ℕ) (target : ℤ) : List (Block n g) →
    List (StoredEntry n) → List (StoredEntry n) → Bool × ℕ
  | [], xs, ys =>
    let size := xs.length + ys.length
…

    Mentions: OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block, OAI.LowSpaceSubsetSum.StoredEntry

  25. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.run_value line 209
  26. def OAI.LowSpaceSubsetSum.StoredSeparatorCheck.factor line 233
  27. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.factor_ge line 237
  28. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.run_work line 241

    Source documentation

    Source scans are the same ledger used by the established expectation bound.

    theorem run_work (capacity : ℕ) (hcap : capacity = 2 ^ n) (target : ℤ)
    (blocks : List (Block n g)) (xs ys : List (StoredEntry n)) :
    (run capacity target blocks xs ys).2 ≤ factor n blocks *
      ((SeparatorBlocks.check n StoredEntry.value StoredEntry.value target
        (blocks.map Block.source) xs ys).scans + xs.length + ys.length + 1) := by
…

    Mentions: OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block, OAI.LowSpaceSubsetSum.StoredEntry, OAI.LowSpaceSubsetSum.StoredSeparatorCheck.run, OAI.LowSpaceSubsetSum.StoredSeparatorCheck.factor, OAI.LowSpaceSubsetSum.SeparatorBlocks.check, OAI.LowSpaceSubsetSum.StoredSeparatorCheck.Block.source

  29. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.factor_add_bound line 277
  30. theorem OAI.LowSpaceSubsetSum.StoredSeparatorCheck.four_factor line 289