OAI/Combinatorics/LowSpaceSubsetSum/Counting/SamplerAttempts.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Counted bounded rejection and deterministic divisor tests

The accumulator counts precisely the candidates actually read, including rejections. It is carried through tail calls and never revisits a candidate.

  1. def OAI.LowSpaceSubsetSum.SamplerAttempts.runAcc line 18
  2. def OAI.LowSpaceSubsetSum.SamplerAttempts.run line 24
  3. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.runAcc_value line 27
  4. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.run_value line 38
  5. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.runAcc_reads line 41
  6. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.run_reads line 53
  7. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.runAcc_exhausted line 57
  8. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.range_reads line 69
  9. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.prime_reads line 72
  10. def OAI.LowSpaceSubsetSum.SamplerAttempts.divisors line 77

    Source documentation

    Search each possible small divisor once, stopping at the first divisor. The numeric square-root bound is a parameter to this counted inner loop.

    def divisors (p : ℕ) : Option ℕ × ℕ :=
…
  11. def OAI.LowSpaceSubsetSum.SamplerAttempts.isPrime line 80
  12. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.isPrime_correct line 82
  13. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.divisor_tests_le line 101
  14. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.divisor_tests_lt_pow line 104
  15. def OAI.LowSpaceSubsetSum.SamplerAttempts.runCostAcc line 114

    Source documentation

    The candidate evaluator returns its Boolean answer and its actual work. Both work counters are accumulator fields, including on exhaustion.

    def runCostAcc (test : Ω → Bool × ℕ) :
    (N : ℕ) → (Fin N → Ω) → ℕ → ℕ → Option Ω × ℕ × ℕ
  | 0, _, reads, work => (none, reads, work)
  | N + 1, f, reads, work =>
    let result := test (f 0)
…
  16. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.runCostAcc_value line 122
  17. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.runCostAcc_bounds line 133
  18. def OAI.LowSpaceSubsetSum.SamplerAttempts.divisorsBits line 161

    Source documentation

    A bit-bounded trial-division implementation. The loop bound is a power of two determined by the candidate width, so no square-root oracle is used. Squares beyond the candidate are discarded by an ordinary multiplication and comparison before divisibility is tested.

    def divisorsBits (ell : ℕ) (p : Fin (2 ^ ell)) : Option ℕ × ℕ :=
…
  19. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.divisorsBits_none line 165
  20. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.divisorsBits_tests line 187
  21. def OAI.LowSpaceSubsetSum.SamplerAttempts.primeTest line 191
  22. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.primeTest_correct line 196
  23. def OAI.LowSpaceSubsetSum.SamplerAttempts.primeRun line 204
  24. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.primeRun_value line 207
  25. theorem OAI.LowSpaceSubsetSum.SamplerAttempts.primeRun_bounds line 214