OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedHistoryBounds.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Resource bounds for the complete executed word history

The seven stages add their retained seed buffers. Exponents are bounded only after this addition, so repeated preparation cannot hide storage.

  1. def OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.workBudget line 23
  2. def OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.liveBudget line 24
  3. theorem OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.polynomial_stage line 26
  4. theorem OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.prepared_stage line 41
  5. theorem OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.family_stage line 55
  6. theorem OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.residues_bounded_scale line 70
  7. theorem OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.guessHistory_budget line 100
  8. theorem OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.partitionHistory_budget line 111
  9. theorem OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.primeHistory_budget line 120
  10. theorem OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.trialHistory_budget line 128
  11. theorem OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.extraHistory_budget line 136
  12. theorem OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.separatorDraws_stage line 144
  13. theorem OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.bucketHistory_budget line 153
  14. theorem OAI.LowSpaceSubsetSum.WordSeedHistoryBounds.bucketHistory_bounded line 161