OAI/Combinatorics/LowSpaceSubsetSum/Storage/ScalarSamplerCells.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

Actual bounded scalar draws with live candidate storage

Each factor uses the explicit finite candidate vector and scalar trial division cursor. Products retain their earlier scalar values and reserve unread random-word tails on failure. The final arrays contain three words.

  1. def OAI.LowSpaceSubsetSum.ScalarSamplerCells.primeFactor line 16
  2. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.primeFactor_value line 21
  3. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.primeFactor_cells line 27
  4. def OAI.LowSpaceSubsetSum.ScalarSamplerCells.factor line 33
  5. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.factor_value line 43
  6. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.factor_cells line 54
  7. def OAI.LowSpaceSubsetSum.ScalarSamplerCells.pairFactors line 65
  8. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.pairFactors_value line 69
  9. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.pairFactors_cells line 75
  10. def OAI.LowSpaceSubsetSum.ScalarSamplerCells.triple line 83
  11. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.triple_value line 88
  12. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.triple_cells line 95
  13. def OAI.LowSpaceSubsetSum.ScalarSamplerCells.nested line 102
  14. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.nested_value line 107
  15. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.nested_cells line 111
  16. def OAI.LowSpaceSubsetSum.ScalarSamplerCells.extra line 117
  17. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.extra_value line 122
  18. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.extra_cells line 126
  19. def OAI.LowSpaceSubsetSum.ScalarSamplerCells.residueTail line 132
  20. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.residueTail_value line 136
  21. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.residueTail_cells line 143
  22. def OAI.LowSpaceSubsetSum.ScalarSamplerCells.residues line 151
  23. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.residues_value line 158
  24. theorem OAI.LowSpaceSubsetSum.ScalarSamplerCells.residues_cells line 167