OAI/Combinatorics/LowSpaceSubsetSum/Word/WordSeedPreparedBind.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Dependent generation with access to the preceding stored seed

This variant permits the next stage to run the already counted layout or parameter preparation on the actual preceding seed. Its charge is part of that stage's Execution, rather than an implicit evaluation of ideal data.

  1. def OAI.LowSpaceSubsetSum.WordSeedMeasured.firstAccepted line 19
  2. def OAI.LowSpaceSubsetSum.WordSeedMeasured.bindSeedRun line 30
  3. def OAI.LowSpaceSubsetSum.WordSeedMeasured.bindSeed line 42
  4. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.bindSeed_bounded line 62
  5. def OAI.LowSpaceSubsetSum.WordSeedMeasured.prepareThen line 79
  6. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.prepareThen_bounded line 88
  7. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.accepted_source line 99

    Source documentation

    The concrete cached value is the successful sampler output.

    theorem accepted_source {S : SamplerCoupling α} (a : Accepted S) :
    S.bounded a.seed.val = some a.value :=
…

    Mentions: OAI.LowSpaceSubsetSum.SamplerCoupling, OAI.LowSpaceSubsetSum.WordSeedMeasured.Accepted

  8. def OAI.LowSpaceSubsetSum.WordSeedMeasured.mapStoredRun line 103
  9. def OAI.LowSpaceSubsetSum.WordSeedMeasured.mapStored line 116
  10. theorem OAI.LowSpaceSubsetSum.WordSeedMeasured.mapStored_bounded line 128