OAI/Combinatorics/LowSpaceSubsetSum/Storage/PrimeTestCells.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Scalar-cursor trial division

The cursor advances by one after a failed divisor test. The loop retains only its fixed scalar state; the candidate enumeration is not materialized. Its returned answer and counter equal the trial-division specification.

  1. def OAI.LowSpaceSubsetSum.PrimeTestCells.scan line 14
  2. theorem OAI.LowSpaceSubsetSum.PrimeTestCells.scan_value line 20
  3. theorem OAI.LowSpaceSubsetSum.PrimeTestCells.scan_cells line 40
  4. def OAI.LowSpaceSubsetSum.PrimeTestCells.divisors line 49
  5. theorem OAI.LowSpaceSubsetSum.PrimeTestCells.divisors_value line 52
  6. def OAI.LowSpaceSubsetSum.PrimeTestCells.test line 60
  7. theorem OAI.LowSpaceSubsetSum.PrimeTestCells.test_value line 65
  8. theorem OAI.LowSpaceSubsetSum.PrimeTestCells.test_cells line 69