OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedStructuralExecution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Measured structural draws in a representation history

Permutation composition and balanced-coloring maps create closures. These closures are not applied during the next prime draw; the prepared action later materializes all queried coordinates with its own counted routines. The guess encoding performs its explicit endpoint arithmetic.

  1. def OAI.LowSpaceSubsetSum.WordSeedMeasured.layout line 20
  2. def OAI.LowSpaceSubsetSum.WordSeedMeasured.guesses line 25
  3. def OAI.LowSpaceSubsetSum.WordSeedMeasured.partition line 32
  4. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.clog_le line 43

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

  5. def OAI.LowSpaceSubsetSum.WordSeedMeasured.partitions line 46
  6. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.layout_bounded line 56
  7. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.guesses_bounded line 70