OAI/Combinatorics/LowSpaceSubsetSum/Separators/PreparedSeparatorContext.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Preparing the shared checker context with computed depths

The four ceiling logarithms are computed by bounded doubling loops. The resulting blocks retain the explicit coordinate vectors and incidence arrays; later checks reuse them without rebuilding the tables.

  1. def OAI.LowSpaceSubsetSum.PreparedSeparatorContext.depths line 19
  2. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorContext.depths_value line 25
  3. def OAI.LowSpaceSubsetSum.PreparedSeparatorContext.prepare line 32
  4. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorContext.prepare_value line 45
  5. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorContext.prepare_work line 53
  6. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorContext.prepare_work_scale line 71
  7. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorContext.acceptance line 88
  8. theorem OAI.LowSpaceSubsetSum.PreparedSeparatorContext.run_work line 103