OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedHistoryExecution.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Executing the dependent representation sampling history

Every continuation uses the cached accepted layout. At the prime stages it runs the counted mixer preparation on that layout's stored accepted seed.

  1. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.clog_le line 17

    Distinct definitions of this name: OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedBucketExecution.lean:14 (same declaration text), OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedStructuralExecution.lean:43 (same statement text; different proof or body). Qualify references as OAI.LowSpaceSubsetSum.WordSeedMeasured.clog_le@path.

  2. def OAI.LowSpaceSubsetSum.WordSeedMeasured.guessHistory line 20
  3. def OAI.LowSpaceSubsetSum.WordSeedMeasured.partitionHistory line 30
  4. def OAI.LowSpaceSubsetSum.WordSeedMeasured.layoutOfPartition line 37
  5. def OAI.LowSpaceSubsetSum.WordSeedMeasured.primeHistory line 45
  6. def OAI.LowSpaceSubsetSum.WordSeedMeasured.residues line 53
  7. def OAI.LowSpaceSubsetSum.WordSeedMeasured.trialHistory line 64
  8. def OAI.LowSpaceSubsetSum.WordSeedMeasured.layoutOfTrial line 72
  9. def OAI.LowSpaceSubsetSum.WordSeedMeasured.extraHistory line 81