OAI/Combinatorics/LowSpaceSubsetSum/Representation/RepresentationEmitCells.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Scratch of the concrete validity-and-entry callback

All masks are bounded index lists. Membership, overlap tests, canonical top mask construction and four signed weights have explicit work counters. Input masks remain shared throughout.

  1. def OAI.LowSpaceSubsetSum.RepresentationEmitCells.disjointAcc line 16
  2. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.disjointAcc_value line 25
  3. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.disjointAcc_cells line 32
  4. def OAI.LowSpaceSubsetSum.RepresentationEmitCells.disjoint line 44
  5. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.disjoint_value line 48
  6. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.disjoint_cells line 51
  7. def OAI.LowSpaceSubsetSum.RepresentationEmitCells.four line 57
  8. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.four_value line 68
  9. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.four_cells line 72
  10. def OAI.LowSpaceSubsetSum.RepresentationEmitCells.valid line 82
  11. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.valid_value line 89
  12. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.valid_cells line 93
  13. def OAI.LowSpaceSubsetSum.RepresentationEmitCells.filterMask line 101
  14. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.filterMask_value line 109
  15. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.filterMask_cells line 116
  16. def OAI.LowSpaceSubsetSum.RepresentationEmitCells.topMask line 125
  17. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.mask_ext line 134
  18. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.topMask_value line 140
  19. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.topMask_cells line 150
  20. def OAI.LowSpaceSubsetSum.RepresentationEmitCells.parentWeight line 158
  21. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.parentWeight_value line 167
  22. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.parentWeight_cells line 172
  23. def OAI.LowSpaceSubsetSum.RepresentationEmitCells.emit line 181
  24. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.emit_value line 191
  25. theorem OAI.LowSpaceSubsetSum.RepresentationEmitCells.emit_cells line 196