OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedStructuralBounds.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Polynomial envelopes for the structural history draws

These bounds charge measured permutation generation and the actual constant size tuple/closure constructors. Materialization is charged by the later preparation stage.

  1. theorem OAI.LowSpaceSubsetSum.WordSeedStructuralBounds.self_le_power line 19
  2. theorem OAI.LowSpaceSubsetSum.WordSeedStructuralBounds.coefficient_power line 22
  3. theorem OAI.LowSpaceSubsetSum.WordSeedStructuralBounds.additive_slack line 25
  4. theorem OAI.LowSpaceSubsetSum.WordSeedStructuralBounds.triple_slack line 30
  5. theorem OAI.LowSpaceSubsetSum.WordSeedStructuralBounds.layout_numeric line 35
  6. theorem OAI.LowSpaceSubsetSum.WordSeedStructuralBounds.guesses_numeric line 46
  7. theorem OAI.LowSpaceSubsetSum.WordSeedStructuralBounds.layout_bounded_scale line 53
  8. theorem OAI.LowSpaceSubsetSum.WordSeedStructuralBounds.guesses_bounded_scale line 60
  9. theorem OAI.LowSpaceSubsetSum.WordSeedStructuralBounds.block_size_le line 67
  10. theorem OAI.LowSpaceSubsetSum.WordSeedStructuralBounds.partition_bounded_scale line 72
  11. theorem OAI.LowSpaceSubsetSum.WordSeedStructuralBounds.partitions_bounded_scale line 90