OAI/Combinatorics/LowSpaceSubsetSum/Separators/PreparedSeparatorWork.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Polynomial work per source scan for the prepared checker

The incidence tables are built once. Each subsequent checker call is the stored-list execution, with its cost bounded by the same source scan ledger that occurs in the separator expectation theorem.

  1. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorWork.queryBound line 19
  2. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorWork.factor line 31
  3. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorWork.factor_scale line 41
  4. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorWork.prepared_steps line 53
  5. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorWork.run_work line 64
  6. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorWork.family_search_bound line 86

    Source documentation

    A fixed integer number of binary-search steps suffices for every table row; it depends only on the local universe size.

    theorem family_search_bound (family : Array (Fin (2 ^ g)))
    (hsize : family.size ≤ 11 * 2 ^ g) : family.size < 2 ^ (g + 4) := by
…